author ballarin Mon Mar 08 12:17:43 2004 +0100 (2004-03-08) changeset 14445 4392cb82018b parent 14444 24724afce166 child 14446 0bc2519e9990
Bug-fixes for transitivity reasoner.
 src/HOL/Library/Multiset.thy file | annotate | diff | revisions src/Provers/order.ML file | annotate | diff | revisions
```     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.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.133 -
2.134 -fun addTermEdge (v,u,[]) = [(v,[u])]
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.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.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.202 -    if u = v then adj else adjacent el u
2.203 -|   adjacent nil _ = []
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.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.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.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.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.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.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 -
```