Bug-fixes for transitivity reasoner.
authorballarin
Mon Mar 08 12:17:43 2004 +0100 (2004-03-08)
changeset 144454392cb82018b
parent 14444 24724afce166
child 14446 0bc2519e9990
Bug-fixes for transitivity reasoner.
src/HOL/Library/Multiset.thy
src/Provers/order.ML
     1.1 --- a/src/HOL/Library/Multiset.thy	Mon Mar 08 12:16:57 2004 +0100
     1.2 +++ b/src/HOL/Library/Multiset.thy	Mon Mar 08 12:17:43 2004 +0100
     1.3 @@ -801,7 +801,6 @@
     1.4      apply (rule one_step_implies_mult)
     1.5        apply (simp only: trans_def)
     1.6        apply auto
     1.7 -  apply (blast intro: order_less_trans)
     1.8    done
     1.9  
    1.10  theorem union_upper1: "A <= A + (B::'a::order multiset)"
     2.1 --- a/src/Provers/order.ML	Mon Mar 08 12:16:57 2004 +0100
     2.2 +++ b/src/Provers/order.ML	Mon Mar 08 12:17:43 2004 +0100
     2.3 @@ -5,7 +5,7 @@
     2.4    Copyright:	TU Muenchen
     2.5  *)
     2.6  
     2.7 -(* TODO: reduce number of input thms, reduce code duplication *)
     2.8 +(* TODO: reduce number of input thms *)
     2.9  
    2.10  (*
    2.11  
    2.12 @@ -73,7 +73,6 @@
    2.13  struct
    2.14  
    2.15  (* Extract subgoal with signature *)
    2.16 -
    2.17  fun SUBGOAL goalfun i st =
    2.18    goalfun (List.nth(prems_of st, i-1),  i, sign_of_thm st) st
    2.19                               handle Subscript => Seq.empty;
    2.20 @@ -84,7 +83,7 @@
    2.21    | Thm of proof list * thm; 
    2.22    
    2.23  exception Cannot;
    2.24 -  (* Internal exception, raised if conclusion cannot be derived from
    2.25 + (* Internal exception, raised if conclusion cannot be derived from
    2.26       assumptions. *)
    2.27  exception Contr of proof;
    2.28    (* Internal exception, raised if contradiction ( x < x ) was derived *)
    2.29 @@ -99,7 +98,6 @@
    2.30     = Less  of term * term * proof 
    2.31     | Le    of term * term * proof
    2.32     | NotEq of term * term * proof; 
    2.33 -
    2.34     
    2.35  (* Misc functions for datatype less *)
    2.36  fun lower (Less (x, _, _)) = x
    2.37 @@ -114,7 +112,6 @@
    2.38  |   getprf   (Le   (_, _, p)) = p
    2.39  |   getprf   (NotEq (_,_, p)) = p;
    2.40  
    2.41 -
    2.42  (* ************************************************************************ *)
    2.43  (*                                                                          *)
    2.44  (* mkasm_partial sign (t, n) : Sign.sg -> (Term.term * int) -> less         *)
    2.45 @@ -138,13 +135,11 @@
    2.46      | "~="  => if (x aconv y) then 
    2.47                    raise Contr (Thm ([(Thm ([(Thm ([], Less.le_refl)) ,(Asm n)], Less.le_neq_trans))], Less.less_reflE))
    2.48                 else [ NotEq (x, y, Asm n),
    2.49 -                      NotEq (y, x,Thm ( [Asm n], thm "not_sym"))] (* Le (x, x, Thm ([],Less.le_refl))]*) 
    2.50 +                      NotEq (y, x,Thm ( [Asm n], thm "not_sym"))] 
    2.51      | _     => error ("partial_tac: unknown relation symbol ``" ^ rel ^
    2.52                   "''returned by decomp_part."))
    2.53    | None => [];
    2.54  
    2.55 -
    2.56 -
    2.57  (* ************************************************************************ *)
    2.58  (*                                                                          *)
    2.59  (* mkasm_linear sign (t, n) : Sign.sg -> (Term.term * int) -> less          *)
    2.60 @@ -175,7 +170,6 @@
    2.61                   "''returned by decomp_lin."))
    2.62    | None => [];
    2.63  
    2.64 -
    2.65  (* ************************************************************************ *)
    2.66  (*                                                                          *)
    2.67  (* mkconcl_partial sign t : Sign.sg -> Term.term -> less                    *)
    2.68 @@ -196,7 +190,6 @@
    2.69      | _  => raise Cannot)
    2.70    | None => raise Cannot;
    2.71  
    2.72 -
    2.73  (* ************************************************************************ *)
    2.74  (*                                                                          *)
    2.75  (* mkconcl_linear sign t : Sign.sg -> Term.term -> less                     *)
    2.76 @@ -219,8 +212,6 @@
    2.77      | _  => raise Cannot)
    2.78    | None => raise Cannot;
    2.79   
    2.80 -
    2.81 -
    2.82  (* ******************************************************************* *)
    2.83  (*                                                                     *)
    2.84  (* mergeLess (less1,less2):  less * less -> less                       *)
    2.85 @@ -342,33 +333,21 @@
    2.86  (*                                                                     *)
    2.87  (* Inequalities are represented by various types of graphs.            *)
    2.88  (*                                                                     *)
    2.89 -(* 1. (Term.term * Term.term list) list                                *)
    2.90 -(*    - Graph of this type is generated from the assumptions,          *)
    2.91 -(*      does not contain information on which edge stems from which    *)
    2.92 -(*      assumption.                                                    *)
    2.93 -(*    - Used to compute strong components.                             *)
    2.94 -(*                                                                     *)
    2.95 -(* 2. (Term.term * (Term.term * less) list) list                       *)
    2.96 +(* 1. (Term.term * (Term.term * less) list) list                       *)
    2.97  (*    - Graph of this type is generated from the assumptions,          *)
    2.98  (*      it does contain information on which edge stems from which     *)
    2.99  (*      assumption.                                                    *)
   2.100 -(*    - Used to reconstruct paths.                                     *)
   2.101 +(*    - Used to compute strongly connected components                  *)
   2.102 +(*    - Used to compute component subgraphs                            *)
   2.103 +(*    - Used for component subgraphs to reconstruct paths in components*)
   2.104  (*                                                                     *)
   2.105 -(* 3. (int * (int * less) list ) list                                  *)
   2.106 +(* 2. (int * (int * less) list ) list                                  *)
   2.107  (*    - Graph of this type is generated from the strong components of  *)
   2.108 -(*      graph of type 2.  It consists of the strong components of      *)
   2.109 -(*      graph 2, where nodes are indices of the components.            *)
   2.110 +(*      graph of type 1.  It consists of the strong components of      *)
   2.111 +(*      graph 1, where nodes are indices of the components.            *)
   2.112  (*      Only edges between components are part of this graph.          *)
   2.113  (*    - Used to reconstruct paths between several components.          *)
   2.114  (*                                                                     *)
   2.115 -(* 4. (int * int list) list                                            *)
   2.116 -(*    - Graph of this type is generated from graph of type 3, but      *)
   2.117 -(*      edge information of type less is removed.                      *)
   2.118 -(*    - Used to                                                        *)
   2.119 -(*      - Compute transposed graphs of type 4.                         *)
   2.120 -(*      - Compute list of components reachable from a component.       *)
   2.121 -(*                                                                     *)
   2.122 -(*                                                                     *)
   2.123  (* ******************************************************************* *)
   2.124  
   2.125     
   2.126 @@ -376,104 +355,48 @@
   2.127  (* Functions for constructing graphs                           *)
   2.128  (* *********************************************************** *)
   2.129  
   2.130 -fun addLessEdge (v,d,[]) = [(v,d)]
   2.131 -|   addLessEdge (v,d,((u,dl)::el)) = if v aconv u then ((v,d@dl)::el)
   2.132 -    else (u,dl):: (addLessEdge(v,d,el));
   2.133 -
   2.134 -fun addTermEdge (v,u,[]) = [(v,[u])]
   2.135 -|   addTermEdge (v,u,((x,adj)::el)) = if v aconv x then (v,u::adj)::el
   2.136 -    else    (x,adj) :: addTermEdge (v,u,el);
   2.137 +fun addEdge (v,d,[]) = [(v,d)]
   2.138 +|   addEdge (v,d,((u,dl)::el)) = if v aconv u then ((v,d@dl)::el)
   2.139 +    else (u,dl):: (addEdge(v,d,el));
   2.140      
   2.141  (* ********************************************************************* *)
   2.142  (*                                                                       *)
   2.143 -(* buildGraphs constructs three graphs from a list of type less:         *)
   2.144 -(*   g1: graph for the <= relation                                       *)
   2.145 -(*   g2: graph for the <= relation with additional information for       *)
   2.146 -(*       proof reconstruction                                            *)
   2.147 -(*   neqEdges: all edges that are candidates for a ~=                    *)
   2.148 +(* mkGraphs constructs from a list of objects of type less a graph g,    *) 
   2.149 +(* by taking all edges that are candidate for a <=, and a list neqE, by  *)
   2.150 +(* taking all edges that are candiate for a ~=                           *)
   2.151  (*                                                                       *)
   2.152  (* ********************************************************************* *)
   2.153  
   2.154 +fun mkGraphs [] = ([],[],[])
   2.155 +|   mkGraphs lessList = 
   2.156 + let
   2.157  
   2.158 -fun buildGraphs ([],g1,g2,neqEdges) = (g1, g2, neqEdges)
   2.159 -|   buildGraphs (l::ls,g1,g2,neqEdges) = case l of 
   2.160 -(Less (x,y,p)) =>(
   2.161 -      let val g1' = addTermEdge (x,y,g1)
   2.162 -       and g2' = addLessEdge (x,[(y,(Less (x, y, p)))],g2)
   2.163 -      in buildGraphs (ls,g1',g2',l::neqEdges) end)
   2.164 +fun buildGraphs ([],leqG,neqG,neqE) = (leqG, neqG, neqE)
   2.165 +|   buildGraphs (l::ls, leqG,neqG, neqE) = case l of 
   2.166 +  (Less (x,y,p)) =>    
   2.167 +       buildGraphs (ls, addEdge (x,[(y,(Less (x, y, p)))],leqG) , 
   2.168 +                        addEdge (x,[(y,(Less (x, y, p)))],neqG), l::neqE) 
   2.169  | (Le (x,y,p)) =>
   2.170 -( let val g1' = addTermEdge (x,y,g1)
   2.171 -       and g2' = addLessEdge (x,[(y,(Le (x, y,p)))],g2)
   2.172 -  in buildGraphs (ls,g1',g2',neqEdges) end)
   2.173 -| (NotEq  (x,y,p)) => (   buildGraphs (ls,g1,g2,l::neqEdges) )
   2.174 +      buildGraphs (ls, addEdge (x,[(y,(Le (x, y,p)))],leqG) , neqG, neqE) 
   2.175 +| (NotEq  (x,y,p)) => 
   2.176 +      buildGraphs (ls, leqG , addEdge (x,[(y,(NotEq (x, y, p)))],neqG), l::neqE) ;
   2.177 +
   2.178 +  in buildGraphs (lessList, [], [], []) end;
   2.179  
   2.180  
   2.181  (* *********************************************************************** *)
   2.182  (*                                                                         *)
   2.183 -(* adjacent_term g u : (Term.term * 'a list ) list -> Term.term -> 'a list *)
   2.184 -(*                                                                         *)
   2.185 -(*                                                                         *)
   2.186 -(* *********************************************************************** *)
   2.187 -
   2.188 -fun adjacent_term ((v,adj)::el) u = 
   2.189 -    if u aconv v then adj else adjacent_term el u
   2.190 -|   adjacent_term nil _ = []
   2.191 -
   2.192 -(* *********************************************************************** *)
   2.193 -(*                                                                         *)
   2.194 -(* adjacent_term g u : (''a * 'b list ) list -> ''a -> 'b list             *)
   2.195 +(* adjacent g u : (''a * 'b list ) list -> ''a -> 'b list                  *)
   2.196  (*                                                                         *)
   2.197  (* List of successors of u in graph g                                      *)
   2.198  (*                                                                         *)
   2.199  (* *********************************************************************** *)
   2.200   
   2.201 -fun adjacent ((v,adj)::el) u = 
   2.202 -    if u = v then adj else adjacent el u
   2.203 -|   adjacent nil _ = []  
   2.204 +fun adjacent eq_comp ((v,adj)::el) u = 
   2.205 +    if eq_comp (u, v) then adj else adjacent eq_comp el u
   2.206 +|   adjacent _  []  _ = []  
   2.207    
   2.208 -
   2.209 -(* *********************************************************************** *)
   2.210 -(*                                                                         *)
   2.211 -(* transpose_term g:                                                       *)
   2.212 -(* (Term.term * Term.term list) list -> (Term.term * Term.term list) list  *)
   2.213 -(*                                                                         *)
   2.214 -(* Computes transposed graph g' from g                                     *)
   2.215 -(* by reversing all edges u -> v to v -> u                                 *)
   2.216 -(*                                                                         *)
   2.217 -(* *********************************************************************** *)
   2.218 -
   2.219 - fun transpose_term g =
   2.220 -  let
   2.221 -   (* Compute list of reversed edges for each adjacency list *)
   2.222 -   fun flip (u,v::el) = (v,u) :: flip (u,el)
   2.223 -     | flip (_,nil) = nil
   2.224 -
   2.225 -   (* Compute adjacency list for node u from the list of edges
   2.226 -      and return a likewise reduced list of edges.  The list of edges
   2.227 -      is searches for edges starting from u, and these edges are removed. *)
   2.228 -   fun gather (u,(v,w)::el) =
   2.229 -    let
   2.230 -     val (adj,edges) = gather (u,el)
   2.231 -    in
   2.232 -      if u aconv v then (w::adj,edges)
   2.233 -      else (adj,(v,w)::edges)
   2.234 -    end
   2.235 -   | gather (_,nil) = (nil,nil)
   2.236 -
   2.237 -   (* For every node in the input graph, call gather to find all reachable
   2.238 -      nodes in the list of edges *)
   2.239 -   fun assemble ((u,_)::el) edges =
   2.240 -       let val (adj,edges) = gather (u,edges)
   2.241 -       in (u,adj) :: assemble el edges
   2.242 -       end
   2.243 -     | assemble nil _ = nil
   2.244 -
   2.245 -   (* Compute, for each adjacency list, the list with reversed edges,
   2.246 -      and concatenate these lists. *)
   2.247 -   val flipped = foldr (op @) ((map flip g),nil)
   2.248 -      
   2.249 - in assemble g flipped  end    
   2.250 -      
   2.251 +     
   2.252  (* *********************************************************************** *)
   2.253  (*                                                                         *)
   2.254  (* transpose g:                                                            *)
   2.255 @@ -484,10 +407,10 @@
   2.256  (*                                                                         *)
   2.257  (* *********************************************************************** *)
   2.258  
   2.259 -fun transpose g =
   2.260 +fun transpose eq_comp g =
   2.261    let
   2.262     (* Compute list of reversed edges for each adjacency list *)
   2.263 -   fun flip (u,v::el) = (v,u) :: flip (u,el)
   2.264 +   fun flip (u,(v,l)::el) = (v,(u,l)) :: flip (u,el)
   2.265       | flip (_,nil) = nil
   2.266     
   2.267     (* Compute adjacency list for node u from the list of edges
   2.268 @@ -497,7 +420,7 @@
   2.269      let
   2.270       val (adj,edges) = gather (u,el)
   2.271      in
   2.272 -     if u = v then (w::adj,edges)
   2.273 +     if eq_comp (u, v) then (w::adj,edges)
   2.274       else (adj,(v,w)::edges)
   2.275      end
   2.276     | gather (_,nil) = (nil,nil)
   2.277 @@ -516,16 +439,19 @@
   2.278   
   2.279   in assemble g flipped end    
   2.280        
   2.281 -      
   2.282 -(* scc_term : (term * term list) list -> term list list *)
   2.283 +(* *********************************************************************** *)
   2.284 +(*                                                                         *)      
   2.285 +(* scc_term : (term * term list) list -> term list list                    *)
   2.286 +(*                                                                         *)
   2.287 +(* The following is based on the algorithm for finding strongly connected  *)
   2.288 +(* components described in Introduction to Algorithms, by Cormon, Leiserson*)
   2.289 +(* and Rivest, section 23.5. The input G is an adjacency list description  *)
   2.290 +(* of a directed graph. The output is a list of the strongly connected     *)
   2.291 +(* components (each a list of vertices).                                   *)          
   2.292 +(*                                                                         *)   
   2.293 +(*                                                                         *)
   2.294 +(* *********************************************************************** *)
   2.295  
   2.296 -(* The following is based on the algorithm for finding strongly
   2.297 -   connected components described in Introduction to Algorithms,
   2.298 -   by Cormon, Leiserson, and Rivest, section 23.5. The input G
   2.299 -   is an adjacency list description of a directed graph. The
   2.300 -   output is a list of the strongly connected components (each a
   2.301 -   list of vertices). *)          
   2.302 -     
   2.303  fun scc_term G =
   2.304       let
   2.305    (* Ordered list of the vertices that DFS has finished with;
   2.306 @@ -547,9 +473,9 @@
   2.307        let
   2.308     val _ = visited := u :: !visited
   2.309     val descendents =
   2.310 -       foldr (fn (v,ds) => if been_visited v then ds
   2.311 +       foldr (fn ((v,l),ds) => if been_visited v then ds
   2.312              else v :: dfs_visit g v @ ds)
   2.313 -        ((adjacent_term g u) ,nil)
   2.314 +        ((adjacent (op aconv) g u) ,nil)
   2.315        in
   2.316     finish := u :: !finish;
   2.317     descendents
   2.318 @@ -564,7 +490,7 @@
   2.319    visited := nil;
   2.320  
   2.321    (* We don't reset finish because its value is used by
   2.322 -     revfold below, and it will never be used again (even
   2.323 +     foldl below, and it will never be used again (even
   2.324       though dfs_visit will continue to modify it). *)
   2.325  
   2.326    (* DFS on the transpose. The vertices returned by
   2.327 @@ -573,7 +499,7 @@
   2.328       list, which is what is returned. *)
   2.329    foldl (fn (comps,u) =>  
   2.330        if been_visited u then comps
   2.331 -      else ((u :: dfs_visit (transpose_term G) u) :: comps))  (nil,(!finish))
   2.332 +      else ((u :: dfs_visit (transpose (op aconv) G) u) :: comps))  (nil,(!finish))
   2.333  end;
   2.334  
   2.335  
   2.336 @@ -586,7 +512,6 @@
   2.337  (*                                                                         *)
   2.338  (* *********************************************************************** *)
   2.339  
   2.340 -
   2.341  fun dfs_int_reachable g u = 
   2.342   let
   2.343    (* List of vertices which have been visited. *)
   2.344 @@ -598,16 +523,16 @@
   2.345        let
   2.346     val _ = visited := u :: !visited
   2.347     val descendents =
   2.348 -       foldr (fn (v,ds) => if been_visited v then ds
   2.349 +       foldr (fn ((v,l),ds) => if been_visited v then ds
   2.350              else v :: dfs_visit g v @ ds)
   2.351 -        ( ((adjacent g u)) ,nil)
   2.352 +        ( ((adjacent (op =) g u)) ,nil)
   2.353     in  descendents end
   2.354   
   2.355   in u :: dfs_visit g u end;
   2.356  
   2.357      
   2.358  fun indexComps components = 
   2.359 -    ListPair.map (fn (a,b) => (b,a)) (components, 0 upto (length components -1));
   2.360 +    ListPair.map (fn (a,b) => (a,b)) (0 upto (length components -1), components);
   2.361  
   2.362  fun indexNodes IndexComp = 
   2.363      flat (map (fn (index, comp) => (map (fn v => (v,index)) comp)) IndexComp);
   2.364 @@ -616,113 +541,35 @@
   2.365  |   getIndex v ((v',k)::vs) = if v aconv v' then k else getIndex v vs; 
   2.366      
   2.367  
   2.368 -(* ***************************************************************** *)
   2.369 -(*                                                                   *)
   2.370 -(* evalcompgraph components g ntc :                                  *)
   2.371 -(* Term.term list list ->                                            *)
   2.372 -(* (Term.term * (Term.term * less) list) list ->                     *)
   2.373 -(* (Term.term * int) list ->  (int * (int * less) list) list         *)
   2.374 -(*                                                                   *)
   2.375 -(*                                                                   *)
   2.376 -(* Computes, from graph g, list of all its components and the list   *)
   2.377 -(* ntc (nodes, index of component) a graph whose nodes are the       *)
   2.378 -(* indices of the components of g.  Egdes of the new graph are       *)
   2.379 -(* only the edges of g linking two components.                       *)
   2.380 -(*                                                                   *)
   2.381 -(* ***************************************************************** *)
   2.382 -
   2.383 -fun evalcompgraph components g ntc = 
   2.384 -    let
   2.385 -    (* Liste (Index der Komponente, Komponente *)
   2.386 -    val IndexComp = indexComps components;
   2.387 -
   2.388 -    (* Compute new graph with the property that it only contains edges
   2.389 -       between components. *)
   2.390 -  
   2.391 -    (* k is index of current start component. *)   
   2.392 -       
   2.393 -    fun processComponent (k, comp) = 
   2.394 -     let
   2.395 -         (* all edges pointing away from the component *)
   2.396 -	   (* (Term.term * less) list *)
   2.397 -	       val allEdges = flat (map (adjacent_term g) comp);
   2.398 -
   2.399 -		(* choose those edges pointing to nodes outside
   2.400 -                   the current component *)
   2.401 -		
   2.402 -		fun selectEdges  [] = []
   2.403 -		|   selectEdges  ((v,l)::es) = let val k' = getIndex v ntc in 
   2.404 -		    if k' = k then selectEdges es else (k', l) :: (selectEdges  es) end;
   2.405 -
   2.406 -		 (* Insert edge into sorted list of edges, where edge is
   2.407 -                    only added if
   2.408 -                    - it is found for the first time
   2.409 -                    - it is a <= edge and no parallel < edge was found earlier
   2.410 -                    - it is a < edge
   2.411 -                 *)
   2.412 -		     
   2.413 -		 fun insert (h,l) [] = [(h,l)]
   2.414 -		 |   insert (h,l) ((k',l')::es) = if h = k' then (
   2.415 -		     case l of (Less (_, _, _)) => (h,l)::es
   2.416 -		     | _  => (case l' of (Less (_, _, _)) => (h,l')::es
   2.417 -	                      | _ => (k',l)::es) )
   2.418 -		     else (k',l'):: insert (h,l) es;
   2.419 -
   2.420 -		 (* Reorganise list of edges such that
   2.421 -                    - duplicate edges are removed
   2.422 -                    - if a < edge and a <= edge exist at the same time,
   2.423 -                      remove <= edge *)
   2.424 -		     
   2.425 -		 fun sortEdges [] sorted = sorted: (int * less) list
   2.426 -		 |   sortEdges (e::es) sorted = sortEdges es (insert e sorted); 
   2.427 -		    
   2.428 -     in 
   2.429 -       (k, (sortEdges (selectEdges allEdges) []))
   2.430 -     end; 
   2.431 -     
   2.432 -	     			       
   2.433 -in map processComponent IndexComp end; 
   2.434 -
   2.435 -(* Remove ``less'' edge info from graph *)
   2.436 -(* type ('a * ('a * less) list) list *)
   2.437 -fun stripOffLess g = map (fn (v, desc) => (v,map (fn (u,l) => u) desc)) g;
   2.438 -
   2.439 -
   2.440  
   2.441  (* *********************************************************************** *)
   2.442  (*                                                                         *)
   2.443 -(* dfs_term g u v:                                                         *)
   2.444 -(* (Term.term  *(Term.term * less) list) list ->                           *)
   2.445 -(* Term.term -> Term.term -> (bool * less list)                            *) 
   2.446 +(* dfs eq_comp g u v:                                                       *)
   2.447 +(* ('a * 'a -> bool) -> ('a  *( 'a * less) list) list ->                   *)
   2.448 +(* 'a -> 'a -> (bool * ('a * less) list)                                   *) 
   2.449  (*                                                                         *)
   2.450  (* Depth first search of v from u.                                         *)
   2.451  (* Returns (true, path(u, v)) if successful, otherwise (false, []).        *)
   2.452  (*                                                                         *)
   2.453  (* *********************************************************************** *)
   2.454  
   2.455 -
   2.456 -fun dfs_term g u v = 
   2.457 +fun dfs eq_comp g u v = 
   2.458   let 
   2.459 -(* TODO: this comment is unclear *)
   2.460 -    (* Liste der gegangenen Kanten, 
   2.461 -       die Kante e die zum Vorgaenger eines Knoten u gehoert ist jene 
   2.462 -       für die gilt (upper e) = u *)
   2.463 -    val pred :  less list ref = ref nil;
   2.464 -    val visited: term list ref = ref nil;
   2.465 +    val pred = ref nil;
   2.466 +    val visited = ref nil;
   2.467      
   2.468 -    fun been_visited v = exists (fn w => w aconv v) (!visited)
   2.469 +    fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
   2.470      
   2.471      fun dfs_visit u' = 
   2.472      let val _ = visited := u' :: (!visited)
   2.473      
   2.474 -    fun update l = let val _ = pred := l ::(!pred) in () end;
   2.475 +    fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end;
   2.476      
   2.477      in if been_visited v then () 
   2.478 -       else (app (fn (v',l) => if been_visited v' then () else (
   2.479 -        update l; 
   2.480 -        dfs_visit v'; ()) )) (adjacent_term g u')
   2.481 -    end
   2.482 -   
   2.483 +    else (app (fn (v',l) => if been_visited v' then () else (
   2.484 +       update (v',l); 
   2.485 +       dfs_visit v'; ()) )) (adjacent eq_comp g u')
   2.486 +     end
   2.487    in 
   2.488      dfs_visit u; 
   2.489      if (been_visited v) then (true, (!pred)) else (false , [])   
   2.490 @@ -743,11 +590,11 @@
   2.491  (* *********************************************************************** *)
   2.492  
   2.493    
   2.494 -fun completeTermPath u v g = 
   2.495 +fun completeTermPath u v g  = 
   2.496    let 
   2.497 +   val (found, tmp) =  dfs (op aconv) g u v ;
   2.498 +   val pred = map snd tmp;
   2.499     
   2.500 -   val (found, pred) = dfs_term g u v;
   2.501 -
   2.502     fun path x y  =
   2.503        let
   2.504   
   2.505 @@ -771,56 +618,20 @@
   2.506    else path u v ) else raise Cannot
   2.507  end;  
   2.508  
   2.509 -
   2.510 +      
   2.511  (* *********************************************************************** *)
   2.512  (*                                                                         *)
   2.513 -(* dfs_int g u v:                                                          *)
   2.514 -(* (int  *(int * less) list) list -> int -> int                            *)
   2.515 -(* -> (bool *(int*  less) list)                                            *) 
   2.516 -(*                                                                         *)
   2.517 -(* Depth first search of v from u.                                         *)
   2.518 -(* Returns (true, path(u, v)) if successful, otherwise (false, []).        *)
   2.519 +(* findProof (sccGraph, neqE, ntc, sccSubgraphs) subgoal:                  *)
   2.520  (*                                                                         *)
   2.521 -(* *********************************************************************** *)
   2.522 -
   2.523 -fun dfs_int g u v = 
   2.524 - let 
   2.525 -    val pred : (int * less ) list ref = ref nil;
   2.526 -    val visited: int list ref = ref nil;
   2.527 -    
   2.528 -    fun been_visited v = exists (fn w => w = v) (!visited)
   2.529 -    
   2.530 -    fun dfs_visit u' = 
   2.531 -    let val _ = visited := u' :: (!visited)
   2.532 -    
   2.533 -    fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end;
   2.534 -    
   2.535 -    in if been_visited v then () 
   2.536 -    else (app (fn (v',l) => if been_visited v' then () else (
   2.537 -       update (v',l); 
   2.538 -       dfs_visit v'; ()) )) (adjacent g u')
   2.539 -    
   2.540 -    end
   2.541 -   
   2.542 -  in 
   2.543 -    dfs_visit u; 
   2.544 -    if (been_visited v) then (true, (!pred)) else (false , [])   
   2.545 -  end;
   2.546 -  
   2.547 -     
   2.548 -(* *********************************************************************** *)
   2.549 +(* (int * (int * less) list) list * less list *  (Term.term * int) list    *)
   2.550 +(* * ((term * (term * less) list) list) list -> Less -> proof              *)
   2.551  (*                                                                         *)
   2.552 -(* findProof (g2,  cg2, neqEdges, components, ntc) subgoal:                *)
   2.553 -(* (Term.term * (Term.term * less) list) list *                            *)
   2.554 -(* (int * (int * less) list) list * less list *  Term.term list list       *)
   2.555 -(* * ( (Term.term * int) -> proof                                          *)
   2.556 -(*                                                                         *)
   2.557 -(* findProof constructs from graphs (g2, cg2) and neqEdges a proof for     *)
   2.558 -(* subgoal.  Raises exception Cannot if this is not possible.              *)
   2.559 +(* findProof constructs from graphs (sccGraph, sccSubgraphs) and neqE a    *)
   2.560 +(* proof for subgoal.  Raises exception Cannot if this is not possible.    *)
   2.561  (*                                                                         *)
   2.562  (* *********************************************************************** *)
   2.563       
   2.564 -fun findProof (g2, cg2, neqEdges, components, ntc ) subgoal =
   2.565 +fun findProof (sccGraph, neqE, ntc, sccSubgraphs) subgoal =
   2.566  let
   2.567     
   2.568   (* complete path x y from component graph *)
   2.569 @@ -838,13 +649,15 @@
   2.570  	       val v = upper edge
   2.571  	   in
   2.572               if (getIndex u ntc) = xi then 
   2.573 -	       (completeTermPath x u g2)@[edge]@(completeTermPath v y' g2)
   2.574 -	     else (rev_completeComponentPath u)@[edge]@(completeTermPath v y' g2)
   2.575 +	       (completeTermPath x u (nth_elem(xi, sccSubgraphs)) )@[edge]
   2.576 +	       @(completeTermPath v y' (nth_elem((getIndex y' ntc),sccSubgraphs)) )
   2.577 +	     else (rev_completeComponentPath u)@[edge]
   2.578 +	          @(completeTermPath v y' (nth_elem((getIndex y' ntc),sccSubgraphs)) )
   2.579             end
   2.580     in  
   2.581        if x aconv y then 
   2.582          [(Le (x, y, (Thm ([], Less.le_refl))))]
   2.583 -      else ( if xi = yi then completeTermPath x y g2
   2.584 +      else ( if xi = yi then completeTermPath x y (nth_elem(xi, sccSubgraphs))
   2.585               else rev_completeComponentPath y )  
   2.586     end;
   2.587  
   2.588 @@ -854,23 +667,23 @@
   2.589  (* Find a path from x through e to y, of weight <                      *)
   2.590  (* ******************************************************************* *) 
   2.591   
   2.592 - fun findLess e x y xi yi Xreachable Yreachable = 
   2.593 + fun findLess e x y xi yi xreachable yreachable = 
   2.594    let val u = lower e 
   2.595        val v = upper e
   2.596        val ui = getIndex u ntc
   2.597        val vi = getIndex v ntc
   2.598              
   2.599    in 
   2.600 -      if ui mem Xreachable andalso vi mem Xreachable andalso 
   2.601 -         ui mem Yreachable andalso vi mem Yreachable then (
   2.602 +      if ui mem xreachable andalso vi mem xreachable andalso 
   2.603 +         ui mem yreachable andalso vi mem yreachable then (
   2.604         
   2.605    (case e of (Less (_, _, _)) =>  
   2.606         let
   2.607 -        val (xufound, xupred) = dfs_int cg2 xi (getIndex u ntc)
   2.608 +        val (xufound, xupred) =  dfs (op =) sccGraph xi (getIndex u ntc)
   2.609  	    in 
   2.610  	     if xufound then (
   2.611  	      let 
   2.612 -	       val (vyfound, vypred) = dfs_int cg2 (getIndex v ntc) yi 
   2.613 +	       val (vyfound, vypred) =  dfs (op =) sccGraph (getIndex v ntc) yi  
   2.614  	      in 
   2.615  	       if vyfound then (
   2.616  	        let 
   2.617 @@ -885,15 +698,15 @@
   2.618  	     else None
   2.619  	    end
   2.620         |  _   => 
   2.621 -         let val (xufound, xupred) = dfs_int cg2 xi (getIndex u ntc)
   2.622 +         let val (uvfound, uvpred) =  dfs (op =) sccGraph (getIndex u ntc) (getIndex v ntc) 
   2.623               in 
   2.624 -	      if xufound then (
   2.625 +	      if uvfound then (
   2.626  	       let 
   2.627 -	        val (uvfound, uvpred) = dfs_int cg2 (getIndex u ntc) (getIndex v ntc)
   2.628 +	        val (xufound, xupred) = dfs (op =) sccGraph xi (getIndex u ntc)
   2.629  	       in
   2.630 -		if uvfound then (
   2.631 +		if xufound then (
   2.632  		 let 
   2.633 -		  val (vyfound, vypred) = dfs_int cg2 (getIndex v ntc) yi
   2.634 +		  val (vyfound, vypred) =  dfs (op =) sccGraph (getIndex v ntc) yi
   2.635  		 in 
   2.636  		  if vyfound then (
   2.637  		   let
   2.638 @@ -918,13 +731,12 @@
   2.639  in
   2.640    (* looking for x <= y: any path from x to y is sufficient *)
   2.641    case subgoal of (Le (x, y, _)) => (
   2.642 -  
   2.643 +  if sccGraph = [] then raise Cannot else ( 
   2.644     let 
   2.645      val xi = getIndex x ntc
   2.646      val yi = getIndex y ntc
   2.647 -    (* sucht im Komponentengraphen einen Weg von der Komponente in der x liegt
   2.648 -       zu der in der y liegt *)
   2.649 -    val (found, pred) = dfs_int cg2 xi yi
   2.650 +    (* searches in sccGraph a path from xi to yi *)
   2.651 +    val (found, pred) = dfs (op =) sccGraph xi yi
   2.652     in 
   2.653      if found then (
   2.654         let val xypath = completeComponentPath x y pred 
   2.655 @@ -938,20 +750,20 @@
   2.656         end )
   2.657       else raise Cannot 
   2.658     end 
   2.659 -   
   2.660 +    )
   2.661     )
   2.662   (* looking for x < y: particular path required, which is not necessarily
   2.663      found by normal dfs *)
   2.664   |   (Less (x, y, _)) => (
   2.665 +  if sccGraph = [] then raise Cannot else (
   2.666     let 
   2.667      val xi = getIndex x ntc
   2.668      val yi = getIndex y ntc
   2.669 -    val cg2' = stripOffLess cg2
   2.670 -    val cg2'_transpose = transpose cg2'
   2.671 -    (* alle von x aus erreichbaren Komponenten *)
   2.672 -    val xreachable = dfs_int_reachable cg2' xi
   2.673 -    (* all comonents reachable from y in the transposed graph cg2' *)
   2.674 -    val yreachable = dfs_int_reachable cg2'_transpose yi
   2.675 +    val sccGraph_transpose = transpose (op =) sccGraph
   2.676 +    (* all components that can be reached from component xi  *)
   2.677 +    val xreachable = dfs_int_reachable sccGraph xi
   2.678 +    (* all comonents reachable from y in the transposed graph sccGraph' *)
   2.679 +    val yreachable = dfs_int_reachable sccGraph_transpose yi
   2.680      (* for all edges u ~= v or u < v check if they are part of path x < y *)
   2.681      fun processNeqEdges [] = raise Cannot 
   2.682      |   processNeqEdges (e::es) = 
   2.683 @@ -959,18 +771,30 @@
   2.684        | _ => processNeqEdges es
   2.685          
   2.686      in 
   2.687 -       processNeqEdges neqEdges 
   2.688 +       processNeqEdges neqE 
   2.689      end
   2.690 - 
   2.691 +  )
   2.692   )
   2.693  | (NotEq (x, y, _)) => (
   2.694 -  
   2.695 -  let val xi = getIndex x ntc 
   2.696 +  (* if there aren't any edges that are candidate for a ~= raise Cannot *)
   2.697 +  if neqE = [] then raise Cannot
   2.698 +  (* if there aren't any edges that are candidate for <= then just search a edge in neqE that implies the subgoal *)
   2.699 +  else if sccSubgraphs = [] then (
   2.700 +     (case (Library.find_first (fn fact => fact subsumes subgoal) neqE, subgoal) of
   2.701 +       ( Some (NotEq (x, y, p)), NotEq (x', y', _)) =>
   2.702 +          if  (x aconv x' andalso y aconv y') then p 
   2.703 +	  else Thm ([p], thm "not_sym")
   2.704 +     | ( Some (Less (x, y, p)), NotEq (x', y', _)) => 
   2.705 +          if x aconv x' andalso y aconv y' then (Thm ([p], Less.less_imp_neq))
   2.706 +          else (Thm ([(Thm ([p], Less.less_imp_neq))], thm "not_sym"))
   2.707 +     | _ => raise Cannot) 
   2.708 +   ) else (
   2.709 +   
   2.710 +   let  val xi = getIndex x ntc 
   2.711          val yi = getIndex y ntc
   2.712 -	val cg2' = stripOffLess cg2
   2.713 -	val cg2'_transpose = transpose cg2'
   2.714 -        val xreachable = dfs_int_reachable cg2' xi
   2.715 -	val yreachable = dfs_int_reachable cg2'_transpose yi
   2.716 +	val sccGraph_transpose = transpose (op =) sccGraph
   2.717 +        val xreachable = dfs_int_reachable sccGraph xi
   2.718 +	val yreachable = dfs_int_reachable sccGraph_transpose yi
   2.719  	
   2.720  	fun processNeqEdges [] = raise Cannot  
   2.721    	|   processNeqEdges (e::es) = (
   2.722 @@ -981,7 +805,7 @@
   2.723  		
   2.724  	    in  
   2.725  	        (* if x ~= y follows from edge e *)
   2.726 -	    	         if e subsumes subgoal then (
   2.727 +	    	if e subsumes subgoal then (
   2.728  		     case e of (Less (u, v, q)) => (
   2.729  		       if u aconv x andalso v aconv y then (Thm ([q], Less.less_imp_neq))
   2.730  		       else (Thm ([(Thm ([q], Less.less_imp_neq))], thm "not_sym"))
   2.731 @@ -994,14 +818,15 @@
   2.732                  (* if SCC_x is linked to SCC_y via edge e *)
   2.733  		 else if ui = xi andalso vi = yi then (
   2.734                     case e of (Less (_, _,_)) => (
   2.735 -		        let val xypath = (completeTermPath x u g2) @ [e] @ (completeTermPath v y g2)
   2.736 +		        let val xypath = (completeTermPath x u (nth_elem(ui, sccSubgraphs)) ) @ [e] @ (completeTermPath v y (nth_elem(vi, sccSubgraphs)) )
   2.737  			    val xyLesss = transPath (tl xypath, hd xypath)
   2.738  			in  (Thm ([getprf xyLesss], Less.less_imp_neq)) end)
   2.739  		   | _ => (   
   2.740 -		        let val xupath = completeTermPath x u g2
   2.741 -			    val uxpath = completeTermPath u x g2
   2.742 -			    val vypath = completeTermPath v y g2
   2.743 -			    val yvpath = completeTermPath y v g2
   2.744 +		        let 
   2.745 +			    val xupath = completeTermPath x u  (nth_elem(ui, sccSubgraphs))
   2.746 +			    val uxpath = completeTermPath u x  (nth_elem(ui, sccSubgraphs))
   2.747 +			    val vypath = completeTermPath v y  (nth_elem(vi, sccSubgraphs))
   2.748 +			    val yvpath = completeTermPath y v  (nth_elem(vi, sccSubgraphs))
   2.749  			    val xuLesss = transPath (tl xupath, hd xupath)     
   2.750  			    val uxLesss = transPath (tl uxpath, hd uxpath)			    
   2.751  			    val vyLesss = transPath (tl vypath, hd vypath)			
   2.752 @@ -1014,15 +839,15 @@
   2.753  			)       
   2.754  		  ) else if ui = yi andalso vi = xi then (
   2.755  		     case e of (Less (_, _,_)) => (
   2.756 -		        let val xypath = (completeTermPath y u g2) @ [e] @ (completeTermPath v x g2)
   2.757 +		        let val xypath = (completeTermPath y u (nth_elem(ui, sccSubgraphs)) ) @ [e] @ (completeTermPath v x (nth_elem(vi, sccSubgraphs)) )
   2.758  			    val xyLesss = transPath (tl xypath, hd xypath)
   2.759  			in (Thm ([(Thm ([getprf xyLesss], Less.less_imp_neq))] , thm "not_sym")) end ) 
   2.760  		     | _ => (
   2.761  		        
   2.762 -			let val yupath = completeTermPath y u g2
   2.763 -			    val uypath = completeTermPath u y g2
   2.764 -			    val vxpath = completeTermPath v x g2
   2.765 -			    val xvpath = completeTermPath x v g2
   2.766 +			let val yupath = completeTermPath y u (nth_elem(ui, sccSubgraphs))
   2.767 +			    val uypath = completeTermPath u y (nth_elem(ui, sccSubgraphs))
   2.768 +			    val vxpath = completeTermPath v x (nth_elem(vi, sccSubgraphs))
   2.769 +			    val xvpath = completeTermPath x v (nth_elem(vi, sccSubgraphs))
   2.770  			    val yuLesss = transPath (tl yupath, hd yupath)     
   2.771  			    val uyLesss = transPath (tl uypath, hd uypath)			    
   2.772  			    val vxLesss = transPath (tl vxpath, hd vxpath)			
   2.773 @@ -1040,43 +865,58 @@
   2.774  		              (Some prf) =>  (Thm ([prf], Less.less_imp_neq))  
   2.775                               | None =>  (
   2.776  		               let 
   2.777 -		                val yr = dfs_int_reachable cg2' yi
   2.778 -	                        val xr = dfs_int_reachable cg2'_transpose xi
   2.779 +		                val yr = dfs_int_reachable sccGraph yi
   2.780 +	                        val xr = dfs_int_reachable sccGraph_transpose xi
   2.781  		               in 
   2.782  		                case  (findLess e y x yi xi yr xr) of 
   2.783  		                      (Some prf) => (Thm ([(Thm ([prf], Less.less_imp_neq))], thm "not_sym")) 
   2.784                                        | _ => processNeqEdges es
   2.785  		               end)
   2.786  		 ) end) 
   2.787 -     in processNeqEdges neqEdges end
   2.788 +     in processNeqEdges neqE end)
   2.789    )    
   2.790  end;
   2.791  
   2.792  
   2.793 -(* *********************************************************************** *)
   2.794 -(*                                                                         *)
   2.795 -(* checkComponents g components ntc neqEdges:                              *)
   2.796 -(* (Term.term * (Term.term * less) list) list -> Term.term list list  ->   *)
   2.797 -(* (Term.term * int) -> less list -> bool                                  *)
   2.798 -(*                                                                         *)
   2.799 -(* For each edge in the list neqEdges check if it leads to a contradiction.*)
   2.800 -(* We have a contradiction for edge u ~= v and u < v if:                   *)
   2.801 -(* - u and v are in the same component,                                    *)
   2.802 -(*   that is, a path u <= v and a path v <= u exist, hence u = v.          *)
   2.803 -(* From irreflexivity of < follows u < u or v < v.  Ex false quodlibet.    *)
   2.804 -(*                                                                         *)
   2.805 -(*                                                                         *)
   2.806 -(* *********************************************************************** *)
   2.807 +(* ******************************************************************* *)
   2.808 +(*                                                                     *)
   2.809 +(* mk_sccGraphs components leqG neqG ntc :                             *)
   2.810 +(* Term.term list list ->                                              *)
   2.811 +(* (Term.term * (Term.term * less) list) list ->                       *)
   2.812 +(* (Term.term * (Term.term * less) list) list ->                       *)
   2.813 +(* (Term.term * int)  list ->                                          *)
   2.814 +(* (int * (int * less) list) list   *                                  *)
   2.815 +(* ((Term.term * (Term.term * less) list) list) list                   *)
   2.816 +(*                                                                     *)
   2.817 +(*                                                                     *)
   2.818 +(* Computes, from graph leqG, list of all its components and the list  *)
   2.819 +(* ntc (nodes, index of component) a graph whose nodes are the         *)
   2.820 +(* indices of the components of g.  Egdes of the new graph are         *)
   2.821 +(* only the edges of g linking two components. Also computes for each  *)
   2.822 +(* component the subgraph of leqG that forms this component.           *)
   2.823 +(*                                                                     *)
   2.824 +(* For each component SCC_i is checked if there exists a edge in neqG  *)
   2.825 +(* that leads to a contradiction.                                      *)
   2.826 +(*                                                                     *)
   2.827 +(* We have a contradiction for edge u ~= v and u < v if:               *)
   2.828 +(* - u and v are in the same component,                                *)
   2.829 +(* that is, a path u <= v and a path v <= u exist, hence u = v.        *)
   2.830 +(* From irreflexivity of < follows u < u or v < v. Ex false quodlibet. *)
   2.831 +(*                                                                     *)
   2.832 +(* ******************************************************************* *)
   2.833  
   2.834 +fun mk_sccGraphs _ [] _ _ = ([],[])
   2.835 +|   mk_sccGraphs components leqG neqG ntc = 
   2.836 +    let
   2.837 +    (* Liste (Index der Komponente, Komponente *)
   2.838 +    val IndexComp = indexComps components;
   2.839  
   2.840 -fun checkComponents g components ntc neqEdges = 
   2.841 - let
   2.842 -    (* Construct proof by contradiction for edge *)
   2.843 -    fun handleContr edge  = 
   2.844 +       
   2.845 +    fun handleContr edge g = 
   2.846         (case edge of 
   2.847            (Less  (x, y, _)) => (
   2.848  	    let 
   2.849 -	     val xxpath = edge :: (completeTermPath y x g)
   2.850 +	     val xxpath = edge :: (completeTermPath y x g )
   2.851  	     val xxLesss = transPath (tl xxpath, hd xxpath)
   2.852  	     val q = getprf xxLesss
   2.853  	    in 
   2.854 @@ -1085,8 +925,8 @@
   2.855  	  )
   2.856          | (NotEq (x, y, _)) => (
   2.857  	    let 
   2.858 -	     val xypath = (completeTermPath x y g)
   2.859 -	     val yxpath = (completeTermPath y x g)
   2.860 +	     val xypath = (completeTermPath x y g )
   2.861 +	     val yxpath = (completeTermPath y x g )
   2.862  	     val xyLesss = transPath (tl xypath, hd xypath)
   2.863  	     val yxLesss = transPath (tl yxpath, hd yxpath)
   2.864               val q = getprf (mergeLess ((mergeLess (edge, xyLesss)),yxLesss )) 
   2.865 @@ -1094,21 +934,75 @@
   2.866  	     raise (Contr (Thm ([q], Less.less_reflE )))
   2.867  	    end  
   2.868  	 )
   2.869 -	| _ =>  error "trans_tac/checkCompoents/handleContr: invalid Contradiction");
   2.870 +	| _ =>  error "trans_tac/handleContr: invalid Contradiction");
   2.871 + 
   2.872 +   	
   2.873 +    (* k is index of the actual component *)   
   2.874 +       
   2.875 +    fun processComponent (k, comp) = 
   2.876 +     let    
   2.877 +        (* all edges with weight <= of the actual component *)  
   2.878 +        val leqEdges = flat (map (adjacent (op aconv) leqG) comp);
   2.879 +        (* all edges with weight ~= of the actual component *)  
   2.880 +        val neqEdges = map snd (flat (map (adjacent (op aconv) neqG) comp));
   2.881  
   2.882 -   (* Check each edge in neqEdges for contradiction.
   2.883 -      If there is a contradiction, call handleContr, otherwise do nothing. *)
   2.884 -    fun checkNeqEdges [] = () 
   2.885 -    |   checkNeqEdges (e::es) = 
   2.886 -        (case e of (Less (u, v, _)) => 
   2.887 -	  if (getIndex u ntc) = (getIndex v ntc) then handleContr e g
   2.888 -          else checkNeqEdges es
   2.889 -        | (NotEq (u, v, _)) =>  
   2.890 -	  if (getIndex u ntc) = (getIndex v ntc) then handleContr e g
   2.891 -          else checkNeqEdges es
   2.892 -        | _ => checkNeqEdges es)
   2.893 -     
   2.894 - in if g = [] then () else checkNeqEdges neqEdges end;
   2.895 +       (* find an edge leading to a contradiction *)   
   2.896 +       fun findContr [] = None
   2.897 +       |   findContr (e::es) = 
   2.898 +		    let val ui = (getIndex (lower e) ntc) 
   2.899 +			val vi = (getIndex (upper e) ntc) 
   2.900 +		    in 
   2.901 +		        if ui = vi then  Some e
   2.902 +		        else findContr es
   2.903 +		    end; 
   2.904 +		   
   2.905 +		(* sort edges into component internal edges and 
   2.906 +		   edges pointing away from the component *)
   2.907 +		fun sortEdges  [] (intern,extern)  = (intern,extern)
   2.908 +		|   sortEdges  ((v,l)::es) (intern, extern) = 
   2.909 +		    let val k' = getIndex v ntc in 
   2.910 +		        if k' = k then 
   2.911 +			    sortEdges es (l::intern, extern)
   2.912 +			else sortEdges  es (intern, (k',l)::extern) end;
   2.913 +		
   2.914 +		(* Insert edge into sorted list of edges, where edge is
   2.915 +                    only added if
   2.916 +                    - it is found for the first time
   2.917 +                    - it is a <= edge and no parallel < edge was found earlier
   2.918 +                    - it is a < edge
   2.919 +                 *)
   2.920 +          	 fun insert (h,l) [] = [(h,l)]
   2.921 +		 |   insert (h,l) ((k',l')::es) = if h = k' then (
   2.922 +		     case l of (Less (_, _, _)) => (h,l)::es
   2.923 +		     | _  => (case l' of (Less (_, _, _)) => (h,l')::es
   2.924 +	                      | _ => (k',l)::es) )
   2.925 +		     else (k',l'):: insert (h,l) es;
   2.926 +		
   2.927 +		(* Reorganise list of edges such that
   2.928 +                    - duplicate edges are removed
   2.929 +                    - if a < edge and a <= edge exist at the same time,
   2.930 +                      remove <= edge *)
   2.931 +    		 fun reOrganizeEdges [] sorted = sorted: (int * less) list
   2.932 +		 |   reOrganizeEdges (e::es) sorted = reOrganizeEdges es (insert e sorted); 
   2.933 +	
   2.934 +                 (* construct the subgraph forming the strongly connected component
   2.935 +		    from the edge list *)    
   2.936 +		 fun sccSubGraph [] g  = g
   2.937 +		 |   sccSubGraph (l::ls) g = 
   2.938 +		          sccSubGraph ls (addEdge ((lower l),[((upper l),l)],g))
   2.939 +		 
   2.940 +		 val (intern, extern) = sortEdges leqEdges ([], []);
   2.941 +                 val subGraph = sccSubGraph intern [];
   2.942 +		  
   2.943 +     in  
   2.944 +         case findContr neqEdges of Some e => handleContr e subGraph
   2.945 +	 | _ => ((k, (reOrganizeEdges (extern) [])), subGraph)
   2.946 +     end; 
   2.947 +  
   2.948 +    val tmp =  map processComponent IndexComp    
   2.949 +in 
   2.950 +     ( (map fst tmp), (map snd tmp))  
   2.951 +end; 
   2.952  
   2.953  (* *********************************************************************** *)
   2.954  (*                                                                         *)
   2.955 @@ -1121,17 +1015,15 @@
   2.956  
   2.957  fun solvePartialOrder sign (asms, concl) =
   2.958   let 
   2.959 -  val (g1, g2, neqEdges) = buildGraphs (asms, [], [],[])
   2.960 -  val components = scc_term g1
   2.961 +  val (leqG, neqG, neqE) = mkGraphs asms
   2.962 +  val components = scc_term leqG
   2.963    val ntc = indexNodes (indexComps components)
   2.964 -  val cg2 = evalcompgraph components g2 ntc
   2.965 +  val (sccGraph, sccSubgraphs) = mk_sccGraphs components leqG neqG ntc 
   2.966   in
   2.967 - (* Check for contradiction within assumptions  *)
   2.968 -  checkComponents g2 components ntc neqEdges;
   2.969 -  let 
   2.970 +   let 
   2.971     val (subgoals, prf) = mkconcl_partial sign concl
   2.972     fun solve facts less =
   2.973 -       (case triv_solv less of None => findProof (g2, cg2, neqEdges, components, ntc) less
   2.974 +       (case triv_solv less of None => findProof (sccGraph, neqE, ntc, sccSubgraphs ) less
   2.975         | Some prf => prf )
   2.976    in
   2.977     map (solve asms) subgoals
   2.978 @@ -1149,25 +1041,22 @@
   2.979  
   2.980  fun solveTotalOrder sign (asms, concl) =
   2.981   let 
   2.982 -  val (g1, g2, neqEdges) = buildGraphs (asms, [], [],[])
   2.983 -  val components = scc_term g1   
   2.984 +  val (leqG, neqG, neqE) = mkGraphs asms
   2.985 +  val components = scc_term leqG   
   2.986    val ntc = indexNodes (indexComps components)
   2.987 -  val cg2 = evalcompgraph components g2 ntc
   2.988 +  val (sccGraph, sccSubgraphs) = mk_sccGraphs components leqG neqG ntc
   2.989   in
   2.990 -  checkComponents g2 components ntc neqEdges;
   2.991 -  let 
   2.992 +   let 
   2.993     val (subgoals, prf) = mkconcl_linear sign concl
   2.994     fun solve facts less =
   2.995 -      (case triv_solv less of None => findProof (g2, cg2, neqEdges, components, ntc) less
   2.996 +      (case triv_solv less of None => findProof (sccGraph, neqE, ntc, sccSubgraphs) less
   2.997        | Some prf => prf )
   2.998    in
   2.999     map (solve asms) subgoals
  2.1000    end
  2.1001   end;
  2.1002 -
  2.1003    
  2.1004 -(* partial_tac - solves linear/total orders *)
  2.1005 -  
  2.1006 +(* partial_tac - solves partial orders *)
  2.1007  val partial_tac = SUBGOAL (fn (A, n, sign) =>
  2.1008   let
  2.1009    val rfrees = map Free (rename_wrt_term A (Logic.strip_params A))
  2.1010 @@ -1186,7 +1075,6 @@
  2.1011        );
  2.1012         
  2.1013  (* linear_tac - solves linear/total orders *)
  2.1014 -  
  2.1015  val linear_tac = SUBGOAL (fn (A, n, sign) =>
  2.1016   let
  2.1017    val rfrees = map Free (rename_wrt_term A (Logic.strip_params A))
  2.1018 @@ -1204,4 +1092,3 @@
  2.1019        | Cannot  => no_tac);
  2.1020         
  2.1021  end;
  2.1022 -