src/Provers/order.ML
author wenzelm
Wed Apr 04 00:11:03 2007 +0200 (2007-04-04)
changeset 22578 b0eb5652f210
parent 19617 7cb4b67d4b97
child 23577 c5b93c69afd3
permissions -rw-r--r--
removed obsolete sign_of/sign_of_thm;
     1 (*
     2   Title:	Transitivity reasoner for partial and linear orders
     3   Id:		$Id$
     4   Author:	Oliver Kutter
     5   Copyright:	TU Muenchen
     6 *)
     7 
     8 (* TODO: reduce number of input thms *)
     9 
    10 (*
    11 
    12 The package provides tactics partial_tac and linear_tac that use all
    13 premises of the form
    14 
    15   t = u, t ~= u, t < u, t <= u, ~(t < u) and ~(t <= u)
    16 
    17 to
    18 1. either derive a contradiction,
    19    in which case the conclusion can be any term,
    20 2. or prove the conclusion, which must be of the same form as the
    21    premises (excluding ~(t < u) and ~(t <= u) for partial orders)
    22 
    23 The package is implemented as an ML functor and thus not limited to the
    24 relation <= and friends.  It can be instantiated to any partial and/or
    25 linear order --- for example, the divisibility relation "dvd".  In
    26 order to instantiate the package for a partial order only, supply
    27 dummy theorems to the rules for linear orders, and don't use
    28 linear_tac!
    29 
    30 *)
    31 
    32 signature LESS_ARITH =
    33 sig
    34   (* Theorems for partial orders *)
    35   val less_reflE: thm  (* x < x ==> P *)
    36   val le_refl: thm  (* x <= x *)
    37   val less_imp_le: thm (* x < y ==> x <= y *)
    38   val eqI: thm (* [| x <= y; y <= x |] ==> x = y *)
    39   val eqD1: thm (* x = y ==> x <= y *)
    40   val eqD2: thm (* x = y ==> y <= x *)
    41   val less_trans: thm  (* [| x < y; y < z |] ==> x < z *)
    42   val less_le_trans: thm  (* [| x < y; y <= z |] ==> x < z *)
    43   val le_less_trans: thm  (* [| x <= y; y < z |] ==> x < z *)
    44   val le_trans: thm  (* [| x <= y; y <= z |] ==> x <= z *)
    45   val le_neq_trans : thm (* [| x <= y ; x ~= y |] ==> x < y *)
    46   val neq_le_trans : thm (* [| x ~= y ; x <= y |] ==> x < y *)
    47   val not_sym : thm (* x ~= y ==> y ~= x *)
    48 
    49   (* Additional theorems for linear orders *)
    50   val not_lessD: thm (* ~(x < y) ==> y <= x *)
    51   val not_leD: thm (* ~(x <= y) ==> y < x *)
    52   val not_lessI: thm (* y <= x  ==> ~(x < y) *)
    53   val not_leI: thm (* y < x  ==> ~(x <= y) *)
    54 
    55   (* Additional theorems for subgoals of form x ~= y *)
    56   val less_imp_neq : thm (* x < y ==> x ~= y *)
    57   val eq_neq_eq_imp_neq : thm (* [| x = u ; u ~= v ; v = z|] ==> x ~= z *)
    58 
    59   (* Analysis of premises and conclusion *)
    60   (* decomp_x (`x Rel y') should yield (x, Rel, y)
    61        where Rel is one of "<", "<=", "~<", "~<=", "=" and "~=",
    62        other relation symbols cause an error message *)
    63   (* decomp_part is used by partial_tac *)
    64   val decomp_part: theory -> term -> (term * string * term) option
    65   (* decomp_lin is used by linear_tac *)
    66   val decomp_lin: theory -> term -> (term * string * term) option
    67 end;
    68 
    69 signature ORDER_TAC  =
    70 sig
    71   val partial_tac: int -> tactic
    72   val linear_tac:  int -> tactic
    73 end;
    74 
    75 functor Order_Tac_Fun (Less: LESS_ARITH): ORDER_TAC =
    76 struct
    77 
    78 (* Extract subgoal with signature *)
    79 fun SUBGOAL goalfun i st =
    80   goalfun (List.nth(prems_of st, i-1),  i, Thm.theory_of_thm st) st
    81                              handle Subscript => Seq.empty;
    82 
    83 (* Internal datatype for the proof *)
    84 datatype proof
    85   = Asm of int 
    86   | Thm of proof list * thm; 
    87   
    88 exception Cannot;
    89  (* Internal exception, raised if conclusion cannot be derived from
    90      assumptions. *)
    91 exception Contr of proof;
    92   (* Internal exception, raised if contradiction ( x < x ) was derived *)
    93 
    94 fun prove asms = 
    95   let fun pr (Asm i) = List.nth (asms, i)
    96   |       pr (Thm (prfs, thm)) = (map pr prfs) MRS thm
    97   in pr end;
    98 
    99 (* Internal datatype for inequalities *)
   100 datatype less 
   101    = Less  of term * term * proof 
   102    | Le    of term * term * proof
   103    | NotEq of term * term * proof; 
   104    
   105 (* Misc functions for datatype less *)
   106 fun lower (Less (x, _, _)) = x
   107   | lower (Le (x, _, _)) = x
   108   | lower (NotEq (x,_,_)) = x;
   109 
   110 fun upper (Less (_, y, _)) = y
   111   | upper (Le (_, y, _)) = y
   112   | upper (NotEq (_,y,_)) = y;
   113 
   114 fun getprf   (Less (_, _, p)) = p
   115 |   getprf   (Le   (_, _, p)) = p
   116 |   getprf   (NotEq (_,_, p)) = p;
   117 
   118 (* ************************************************************************ *)
   119 (*                                                                          *)
   120 (* mkasm_partial sign (t, n) : theory -> (Term.term * int) -> less          *)
   121 (*                                                                          *)
   122 (* Tuple (t, n) (t an assumption, n its index in the assumptions) is        *)
   123 (* translated to an element of type less.                                   *)
   124 (* Partial orders only.                                                     *)
   125 (*                                                                          *)
   126 (* ************************************************************************ *)
   127 
   128 fun mkasm_partial sign (t, n) =
   129   case Less.decomp_part sign t of
   130     SOME (x, rel, y) => (case rel of
   131       "<"   => if (x aconv y) then raise Contr (Thm ([Asm n], Less.less_reflE)) 
   132                else [Less (x, y, Asm n)]
   133     | "~<"  => []
   134     | "<="  => [Le (x, y, Asm n)]
   135     | "~<=" => [] 
   136     | "="   => [Le (x, y, Thm ([Asm n], Less.eqD1)),
   137                 Le (y, x, Thm ([Asm n], Less.eqD2))]
   138     | "~="  => if (x aconv y) then 
   139                   raise Contr (Thm ([(Thm ([(Thm ([], Less.le_refl)) ,(Asm n)], Less.le_neq_trans))], Less.less_reflE))
   140                else [ NotEq (x, y, Asm n),
   141                       NotEq (y, x,Thm ( [Asm n], Less.not_sym))] 
   142     | _     => error ("partial_tac: unknown relation symbol ``" ^ rel ^
   143                  "''returned by decomp_part."))
   144   | NONE => [];
   145 
   146 (* ************************************************************************ *)
   147 (*                                                                          *)
   148 (* mkasm_linear sign (t, n) : theory -> (Term.term * int) -> less           *)
   149 (*                                                                          *)
   150 (* Tuple (t, n) (t an assumption, n its index in the assumptions) is        *)
   151 (* translated to an element of type less.                                   *)
   152 (* Linear orders only.                                                      *)
   153 (*                                                                          *)
   154 (* ************************************************************************ *)
   155  
   156 fun mkasm_linear sign (t, n) =
   157   case Less.decomp_lin sign t of
   158     SOME (x, rel, y) => (case rel of
   159       "<"   => if (x aconv y) then raise Contr (Thm ([Asm n], Less.less_reflE)) 
   160                else [Less (x, y, Asm n)]
   161     | "~<"  => [Le (y, x, Thm ([Asm n], Less.not_lessD))]
   162     | "<="  => [Le (x, y, Asm n)]
   163     | "~<=" => if (x aconv y) then 
   164                   raise (Contr (Thm ([Thm ([Asm n], Less.not_leD)], Less.less_reflE))) 
   165                else [Less (y, x, Thm ([Asm n], Less.not_leD))] 
   166     | "="   => [Le (x, y, Thm ([Asm n], Less.eqD1)),
   167                 Le (y, x, Thm ([Asm n], Less.eqD2))]
   168     | "~="  => if (x aconv y) then 
   169                   raise Contr (Thm ([(Thm ([(Thm ([], Less.le_refl)) ,(Asm n)], Less.le_neq_trans))], Less.less_reflE))
   170                else [ NotEq (x, y, Asm n),
   171                       NotEq (y, x,Thm ( [Asm n], Less.not_sym))] 
   172     | _     => error ("linear_tac: unknown relation symbol ``" ^ rel ^
   173                  "''returned by decomp_lin."))
   174   | NONE => [];
   175 
   176 (* ************************************************************************ *)
   177 (*                                                                          *)
   178 (* mkconcl_partial sign t : theory -> Term.term -> less                     *)
   179 (*                                                                          *)
   180 (* Translates conclusion t to an element of type less.                      *)
   181 (* Partial orders only.                                                     *)
   182 (*                                                                          *)
   183 (* ************************************************************************ *)
   184 
   185 fun mkconcl_partial sign t =
   186   case Less.decomp_part sign t of
   187     SOME (x, rel, y) => (case rel of
   188       "<"   => ([Less (x, y, Asm ~1)], Asm 0)
   189     | "<="  => ([Le (x, y, Asm ~1)], Asm 0)
   190     | "="   => ([Le (x, y, Asm ~1), Le (y, x, Asm ~1)],
   191                  Thm ([Asm 0, Asm 1], Less.eqI))
   192     | "~="  => ([NotEq (x,y, Asm ~1)], Asm 0)
   193     | _  => raise Cannot)
   194   | NONE => raise Cannot;
   195 
   196 (* ************************************************************************ *)
   197 (*                                                                          *)
   198 (* mkconcl_linear sign t : theory -> Term.term -> less                      *)
   199 (*                                                                          *)
   200 (* Translates conclusion t to an element of type less.                      *)
   201 (* Linear orders only.                                                      *)
   202 (*                                                                          *)
   203 (* ************************************************************************ *)
   204 
   205 fun mkconcl_linear sign t =
   206   case Less.decomp_lin sign t of
   207     SOME (x, rel, y) => (case rel of
   208       "<"   => ([Less (x, y, Asm ~1)], Asm 0)
   209     | "~<"  => ([Le (y, x, Asm ~1)], Thm ([Asm 0], Less.not_lessI))
   210     | "<="  => ([Le (x, y, Asm ~1)], Asm 0)
   211     | "~<=" => ([Less (y, x, Asm ~1)], Thm ([Asm 0], Less.not_leI))
   212     | "="   => ([Le (x, y, Asm ~1), Le (y, x, Asm ~1)],
   213                  Thm ([Asm 0, Asm 1], Less.eqI))
   214     | "~="  => ([NotEq (x,y, Asm ~1)], Asm 0)
   215     | _  => raise Cannot)
   216   | NONE => raise Cannot;
   217  
   218 (* ******************************************************************* *)
   219 (*                                                                     *)
   220 (* mergeLess (less1,less2):  less * less -> less                       *)
   221 (*                                                                     *)
   222 (* Merge to elements of type less according to the following rules     *)
   223 (*                                                                     *)
   224 (* x <  y && y <  z ==> x < z                                          *)
   225 (* x <  y && y <= z ==> x < z                                          *)
   226 (* x <= y && y <  z ==> x < z                                          *)
   227 (* x <= y && y <= z ==> x <= z                                         *)
   228 (* x <= y && x ~= y ==> x < y                                          *)
   229 (* x ~= y && x <= y ==> x < y                                          *)
   230 (* x <  y && x ~= y ==> x < y                                          *)
   231 (* x ~= y && x <  y ==> x < y                                          *)
   232 (*                                                                     *)
   233 (* ******************************************************************* *)
   234 
   235 fun mergeLess (Less (x, _, p) , Less (_ , z, q)) =
   236       Less (x, z, Thm ([p,q] , Less.less_trans))
   237 |   mergeLess (Less (x, _, p) , Le (_ , z, q)) =
   238       Less (x, z, Thm ([p,q] , Less.less_le_trans))
   239 |   mergeLess (Le (x, _, p) , Less (_ , z, q)) =
   240       Less (x, z, Thm ([p,q] , Less.le_less_trans))
   241 |   mergeLess (Le (x, z, p) , NotEq (x', z', q)) =
   242       if (x aconv x' andalso z aconv z' ) 
   243       then Less (x, z, Thm ([p,q] , Less.le_neq_trans))
   244       else error "linear/partial_tac: internal error le_neq_trans"
   245 |   mergeLess (NotEq (x, z, p) , Le (x' , z', q)) =
   246       if (x aconv x' andalso z aconv z') 
   247       then Less (x, z, Thm ([p,q] , Less.neq_le_trans))
   248       else error "linear/partial_tac: internal error neq_le_trans"
   249 |   mergeLess (NotEq (x, z, p) , Less (x' , z', q)) =
   250       if (x aconv x' andalso z aconv z') 
   251       then Less ((x' , z', q))
   252       else error "linear/partial_tac: internal error neq_less_trans"
   253 |   mergeLess (Less (x, z, p) , NotEq (x', z', q)) =
   254       if (x aconv x' andalso z aconv z') 
   255       then Less (x, z, p)
   256       else error "linear/partial_tac: internal error less_neq_trans"
   257 |   mergeLess (Le (x, _, p) , Le (_ , z, q)) =
   258       Le (x, z, Thm ([p,q] , Less.le_trans))
   259 |   mergeLess (_, _) =
   260       error "linear/partial_tac: internal error: undefined case";
   261 
   262 
   263 (* ******************************************************************** *)
   264 (* tr checks for valid transitivity step                                *)
   265 (* ******************************************************************** *)
   266 
   267 infix tr;
   268 fun (Less (_, y, _)) tr (Le (x', _, _))   = ( y aconv x' )
   269   | (Le   (_, y, _)) tr (Less (x', _, _)) = ( y aconv x' )
   270   | (Less (_, y, _)) tr (Less (x', _, _)) = ( y aconv x' )
   271   | (Le (_, y, _))   tr (Le (x', _, _))   = ( y aconv x' )
   272   | _ tr _ = false;
   273   
   274   
   275 (* ******************************************************************* *)
   276 (*                                                                     *)
   277 (* transPath (Lesslist, Less): (less list * less) -> less              *)
   278 (*                                                                     *)
   279 (* If a path represented by a list of elements of type less is found,  *)
   280 (* this needs to be contracted to a single element of type less.       *)
   281 (* Prior to each transitivity step it is checked whether the step is   *)
   282 (* valid.                                                              *)
   283 (*                                                                     *)
   284 (* ******************************************************************* *)
   285 
   286 fun transPath ([],lesss) = lesss
   287 |   transPath (x::xs,lesss) =
   288       if lesss tr x then transPath (xs, mergeLess(lesss,x))
   289       else error "linear/partial_tac: internal error transpath";
   290   
   291 (* ******************************************************************* *)
   292 (*                                                                     *)
   293 (* less1 subsumes less2 : less -> less -> bool                         *)
   294 (*                                                                     *)
   295 (* subsumes checks whether less1 implies less2                         *)
   296 (*                                                                     *)
   297 (* ******************************************************************* *)
   298   
   299 infix subsumes;
   300 fun (Less (x, y, _)) subsumes (Le (x', y', _)) =
   301       (x aconv x' andalso y aconv y')
   302   | (Less (x, y, _)) subsumes (Less (x', y', _)) =
   303       (x aconv x' andalso y aconv y')
   304   | (Le (x, y, _)) subsumes (Le (x', y', _)) =
   305       (x aconv x' andalso y aconv y')
   306   | (Less (x, y, _)) subsumes (NotEq (x', y', _)) =
   307       (x aconv x' andalso y aconv y') orelse (y aconv x' andalso x aconv y')
   308   | (NotEq (x, y, _)) subsumes (NotEq (x', y', _)) =
   309       (x aconv x' andalso y aconv y') orelse (y aconv x' andalso x aconv y')
   310   | (Le _) subsumes (Less _) =
   311       error "linear/partial_tac: internal error: Le cannot subsume Less"
   312   | _ subsumes _ = false;
   313 
   314 (* ******************************************************************* *)
   315 (*                                                                     *)
   316 (* triv_solv less1 : less ->  proof option                     *)
   317 (*                                                                     *)
   318 (* Solves trivial goal x <= x.                                         *)
   319 (*                                                                     *)
   320 (* ******************************************************************* *)
   321 
   322 fun triv_solv (Le (x, x', _)) =
   323     if x aconv x' then  SOME (Thm ([], Less.le_refl)) 
   324     else NONE
   325 |   triv_solv _ = NONE;
   326 
   327 (* ********************************************************************* *)
   328 (* Graph functions                                                       *)
   329 (* ********************************************************************* *)
   330 
   331 
   332 
   333 (* ******************************************************************* *)
   334 (*                                                                     *)
   335 (* General:                                                            *)
   336 (*                                                                     *)
   337 (* Inequalities are represented by various types of graphs.            *)
   338 (*                                                                     *)
   339 (* 1. (Term.term * (Term.term * less) list) list                       *)
   340 (*    - Graph of this type is generated from the assumptions,          *)
   341 (*      it does contain information on which edge stems from which     *)
   342 (*      assumption.                                                    *)
   343 (*    - Used to compute strongly connected components                  *)
   344 (*    - Used to compute component subgraphs                            *)
   345 (*    - Used for component subgraphs to reconstruct paths in components*)
   346 (*                                                                     *)
   347 (* 2. (int * (int * less) list ) list                                  *)
   348 (*    - Graph of this type is generated from the strong components of  *)
   349 (*      graph of type 1.  It consists of the strong components of      *)
   350 (*      graph 1, where nodes are indices of the components.            *)
   351 (*      Only edges between components are part of this graph.          *)
   352 (*    - Used to reconstruct paths between several components.          *)
   353 (*                                                                     *)
   354 (* ******************************************************************* *)
   355 
   356    
   357 (* *********************************************************** *)
   358 (* Functions for constructing graphs                           *)
   359 (* *********************************************************** *)
   360 
   361 fun addEdge (v,d,[]) = [(v,d)]
   362 |   addEdge (v,d,((u,dl)::el)) = if v aconv u then ((v,d@dl)::el)
   363     else (u,dl):: (addEdge(v,d,el));
   364     
   365 (* ********************************************************************* *)
   366 (*                                                                       *)
   367 (* mkGraphs constructs from a list of objects of type less a graph g,    *) 
   368 (* by taking all edges that are candidate for a <=, and a list neqE, by  *)
   369 (* taking all edges that are candiate for a ~=                           *)
   370 (*                                                                       *)
   371 (* ********************************************************************* *)
   372 
   373 fun mkGraphs [] = ([],[],[])
   374 |   mkGraphs lessList = 
   375  let
   376 
   377 fun buildGraphs ([],leqG,neqG,neqE) = (leqG, neqG, neqE)
   378 |   buildGraphs (l::ls, leqG,neqG, neqE) = case l of 
   379   (Less (x,y,p)) =>    
   380        buildGraphs (ls, addEdge (x,[(y,(Less (x, y, p)))],leqG) , 
   381                         addEdge (x,[(y,(Less (x, y, p)))],neqG), l::neqE) 
   382 | (Le (x,y,p)) =>
   383       buildGraphs (ls, addEdge (x,[(y,(Le (x, y,p)))],leqG) , neqG, neqE) 
   384 | (NotEq  (x,y,p)) => 
   385       buildGraphs (ls, leqG , addEdge (x,[(y,(NotEq (x, y, p)))],neqG), l::neqE) ;
   386 
   387   in buildGraphs (lessList, [], [], []) end;
   388 
   389 
   390 (* *********************************************************************** *)
   391 (*                                                                         *)
   392 (* adjacent g u : (''a * 'b list ) list -> ''a -> 'b list                  *)
   393 (*                                                                         *)
   394 (* List of successors of u in graph g                                      *)
   395 (*                                                                         *)
   396 (* *********************************************************************** *)
   397  
   398 fun adjacent eq_comp ((v,adj)::el) u = 
   399     if eq_comp (u, v) then adj else adjacent eq_comp el u
   400 |   adjacent _  []  _ = []  
   401   
   402      
   403 (* *********************************************************************** *)
   404 (*                                                                         *)
   405 (* transpose g:                                                            *)
   406 (* (''a * ''a list) list -> (''a * ''a list) list                          *)
   407 (*                                                                         *)
   408 (* Computes transposed graph g' from g                                     *)
   409 (* by reversing all edges u -> v to v -> u                                 *)
   410 (*                                                                         *)
   411 (* *********************************************************************** *)
   412 
   413 fun transpose eq_comp g =
   414   let
   415    (* Compute list of reversed edges for each adjacency list *)
   416    fun flip (u,(v,l)::el) = (v,(u,l)) :: flip (u,el)
   417      | flip (_,nil) = nil
   418    
   419    (* Compute adjacency list for node u from the list of edges
   420       and return a likewise reduced list of edges.  The list of edges
   421       is searches for edges starting from u, and these edges are removed. *)
   422    fun gather (u,(v,w)::el) =
   423     let
   424      val (adj,edges) = gather (u,el)
   425     in
   426      if eq_comp (u, v) then (w::adj,edges)
   427      else (adj,(v,w)::edges)
   428     end
   429    | gather (_,nil) = (nil,nil)
   430 
   431    (* For every node in the input graph, call gather to find all reachable
   432       nodes in the list of edges *)
   433    fun assemble ((u,_)::el) edges =
   434        let val (adj,edges) = gather (u,edges)
   435        in (u,adj) :: assemble el edges
   436        end
   437      | assemble nil _ = nil
   438 
   439    (* Compute, for each adjacency list, the list with reversed edges,
   440       and concatenate these lists. *)
   441    val flipped = foldr (op @) nil (map flip g)
   442  
   443  in assemble g flipped end    
   444       
   445 (* *********************************************************************** *)
   446 (*                                                                         *)      
   447 (* scc_term : (term * term list) list -> term list list                    *)
   448 (*                                                                         *)
   449 (* The following is based on the algorithm for finding strongly connected  *)
   450 (* components described in Introduction to Algorithms, by Cormon, Leiserson*)
   451 (* and Rivest, section 23.5. The input G is an adjacency list description  *)
   452 (* of a directed graph. The output is a list of the strongly connected     *)
   453 (* components (each a list of vertices).                                   *)          
   454 (*                                                                         *)   
   455 (*                                                                         *)
   456 (* *********************************************************************** *)
   457 
   458 fun scc_term G =
   459      let
   460   (* Ordered list of the vertices that DFS has finished with;
   461      most recently finished goes at the head. *)
   462   val finish : term list ref = ref nil
   463 
   464   (* List of vertices which have been visited. *)
   465   val visited : term list ref = ref nil
   466   
   467   fun been_visited v = exists (fn w => w aconv v) (!visited)
   468   
   469   (* Given the adjacency list rep of a graph (a list of pairs),
   470      return just the first element of each pair, yielding the 
   471      vertex list. *)
   472   val members = map (fn (v,_) => v)
   473 
   474   (* Returns the nodes in the DFS tree rooted at u in g *)
   475   fun dfs_visit g u : term list =
   476       let
   477    val _ = visited := u :: !visited
   478    val descendents =
   479        foldr (fn ((v,l),ds) => if been_visited v then ds
   480             else v :: dfs_visit g v @ ds)
   481         nil (adjacent (op aconv) g u)
   482       in
   483    finish := u :: !finish;
   484    descendents
   485       end
   486      in
   487 
   488   (* DFS on the graph; apply dfs_visit to each vertex in
   489      the graph, checking first to make sure the vertex is
   490      as yet unvisited. *)
   491   app (fn u => if been_visited u then ()
   492         else (dfs_visit G u; ()))  (members G);
   493   visited := nil;
   494 
   495   (* We don't reset finish because its value is used by
   496      foldl below, and it will never be used again (even
   497      though dfs_visit will continue to modify it). *)
   498 
   499   (* DFS on the transpose. The vertices returned by
   500      dfs_visit along with u form a connected component. We
   501      collect all the connected components together in a
   502      list, which is what is returned. *)
   503   Library.foldl (fn (comps,u) =>  
   504       if been_visited u then comps
   505       else ((u :: dfs_visit (transpose (op aconv) G) u) :: comps))  (nil,(!finish))
   506 end;
   507 
   508 
   509 (* *********************************************************************** *)
   510 (*                                                                         *)
   511 (* dfs_int_reachable g u:                                                  *)
   512 (* (int * int list) list -> int -> int list                                *) 
   513 (*                                                                         *)
   514 (* Computes list of all nodes reachable from u in g.                       *)
   515 (*                                                                         *)
   516 (* *********************************************************************** *)
   517 
   518 fun dfs_int_reachable g u = 
   519  let
   520   (* List of vertices which have been visited. *)
   521   val visited : int list ref = ref nil
   522   
   523   fun been_visited v = exists (fn w => w = v) (!visited)
   524 
   525   fun dfs_visit g u : int list =
   526       let
   527    val _ = visited := u :: !visited
   528    val descendents =
   529        foldr (fn ((v,l),ds) => if been_visited v then ds
   530             else v :: dfs_visit g v @ ds)
   531         nil (adjacent (op =) g u)
   532    in  descendents end
   533  
   534  in u :: dfs_visit g u end;
   535 
   536     
   537 fun indexComps components = 
   538     ListPair.map (fn (a,b) => (a,b)) (0 upto (length components -1), components);
   539 
   540 fun indexNodes IndexComp = 
   541     List.concat (map (fn (index, comp) => (map (fn v => (v,index)) comp)) IndexComp);
   542     
   543 fun getIndex v [] = ~1
   544 |   getIndex v ((v',k)::vs) = if v aconv v' then k else getIndex v vs; 
   545     
   546 
   547 
   548 (* *********************************************************************** *)
   549 (*                                                                         *)
   550 (* dfs eq_comp g u v:                                                       *)
   551 (* ('a * 'a -> bool) -> ('a  *( 'a * less) list) list ->                   *)
   552 (* 'a -> 'a -> (bool * ('a * less) list)                                   *) 
   553 (*                                                                         *)
   554 (* Depth first search of v from u.                                         *)
   555 (* Returns (true, path(u, v)) if successful, otherwise (false, []).        *)
   556 (*                                                                         *)
   557 (* *********************************************************************** *)
   558 
   559 fun dfs eq_comp g u v = 
   560  let 
   561     val pred = ref nil;
   562     val visited = ref nil;
   563     
   564     fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
   565     
   566     fun dfs_visit u' = 
   567     let val _ = visited := u' :: (!visited)
   568     
   569     fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end;
   570     
   571     in if been_visited v then () 
   572     else (app (fn (v',l) => if been_visited v' then () else (
   573        update (v',l); 
   574        dfs_visit v'; ()) )) (adjacent eq_comp g u')
   575      end
   576   in 
   577     dfs_visit u; 
   578     if (been_visited v) then (true, (!pred)) else (false , [])   
   579   end;
   580 
   581   
   582 (* *********************************************************************** *)
   583 (*                                                                         *)
   584 (* completeTermPath u v g:                                                 *)
   585 (* Term.term -> Term.term -> (Term.term * (Term.term * less) list) list    *) 
   586 (* -> less list                                                            *)
   587 (*                                                                         *)
   588 (* Complete the path from u to v in graph g.  Path search is performed     *)
   589 (* with dfs_term g u v.  This yields for each node v' its predecessor u'   *)
   590 (* and the edge u' -> v'.  Allows traversing graph backwards from v and    *)
   591 (* finding the path u -> v.                                                *)
   592 (*                                                                         *)
   593 (* *********************************************************************** *)
   594 
   595   
   596 fun completeTermPath u v g  = 
   597   let 
   598    val (found, tmp) =  dfs (op aconv) g u v ;
   599    val pred = map snd tmp;
   600    
   601    fun path x y  =
   602       let
   603  
   604       (* find predecessor u of node v and the edge u -> v *)
   605 
   606       fun lookup v [] = raise Cannot
   607       |   lookup v (e::es) = if (upper e) aconv v then e else lookup v es;
   608 
   609       (* traverse path backwards and return list of visited edges *)   
   610       fun rev_path v = 
   611        let val l = lookup v pred
   612            val u = lower l;
   613        in
   614         if u aconv x then [l]
   615         else (rev_path u) @ [l] 
   616        end
   617      in rev_path y end;
   618        
   619   in 
   620   if found then (if u aconv v then [(Le (u, v, (Thm ([], Less.le_refl))))]
   621   else path u v ) else raise Cannot
   622 end;  
   623 
   624       
   625 (* *********************************************************************** *)
   626 (*                                                                         *)
   627 (* findProof (sccGraph, neqE, ntc, sccSubgraphs) subgoal:                  *)
   628 (*                                                                         *)
   629 (* (int * (int * less) list) list * less list *  (Term.term * int) list    *)
   630 (* * ((term * (term * less) list) list) list -> Less -> proof              *)
   631 (*                                                                         *)
   632 (* findProof constructs from graphs (sccGraph, sccSubgraphs) and neqE a    *)
   633 (* proof for subgoal.  Raises exception Cannot if this is not possible.    *)
   634 (*                                                                         *)
   635 (* *********************************************************************** *)
   636      
   637 fun findProof (sccGraph, neqE, ntc, sccSubgraphs) subgoal =
   638 let
   639    
   640  (* complete path x y from component graph *)
   641  fun completeComponentPath x y predlist = 
   642    let         
   643 	  val xi = getIndex x ntc
   644 	  val yi = getIndex y ntc 
   645 	  
   646 	  fun lookup k [] =  raise Cannot
   647 	  |   lookup k ((h,l)::us) = if k = h then l else lookup k us;	  
   648 	  
   649 	  fun rev_completeComponentPath y' = 
   650 	   let val edge = lookup (getIndex y' ntc) predlist
   651 	       val u = lower edge
   652 	       val v = upper edge
   653 	   in
   654              if (getIndex u ntc) = xi then 
   655 	       (completeTermPath x u (List.nth(sccSubgraphs, xi)) )@[edge]
   656 	       @(completeTermPath v y' (List.nth(sccSubgraphs, getIndex y' ntc)) )
   657 	     else (rev_completeComponentPath u)@[edge]
   658 	          @(completeTermPath v y' (List.nth(sccSubgraphs, getIndex y' ntc)) )
   659            end
   660    in  
   661       if x aconv y then 
   662         [(Le (x, y, (Thm ([], Less.le_refl))))]
   663       else ( if xi = yi then completeTermPath x y (List.nth(sccSubgraphs, xi))
   664              else rev_completeComponentPath y )  
   665    end;
   666 
   667 (* ******************************************************************* *) 
   668 (* findLess e x y xi yi xreachable yreachable                          *)
   669 (*                                                                     *)
   670 (* Find a path from x through e to y, of weight <                      *)
   671 (* ******************************************************************* *) 
   672  
   673  fun findLess e x y xi yi xreachable yreachable = 
   674   let val u = lower e 
   675       val v = upper e
   676       val ui = getIndex u ntc
   677       val vi = getIndex v ntc
   678             
   679   in 
   680       if ui mem xreachable andalso vi mem xreachable andalso 
   681          ui mem yreachable andalso vi mem yreachable then (
   682        
   683   (case e of (Less (_, _, _)) =>  
   684        let
   685         val (xufound, xupred) =  dfs (op =) sccGraph xi (getIndex u ntc)
   686 	    in 
   687 	     if xufound then (
   688 	      let 
   689 	       val (vyfound, vypred) =  dfs (op =) sccGraph (getIndex v ntc) yi  
   690 	      in 
   691 	       if vyfound then (
   692 	        let 
   693 	         val xypath = (completeComponentPath x u xupred)@[e]@(completeComponentPath v y vypred)
   694 	         val xyLesss = transPath (tl xypath, hd xypath)
   695 	        in 
   696 		 if xyLesss subsumes subgoal then SOME (getprf xyLesss) 
   697                  else NONE
   698 	       end)
   699 	       else NONE
   700 	      end)
   701 	     else NONE
   702 	    end
   703        |  _   => 
   704          let val (uvfound, uvpred) =  dfs (op =) sccGraph (getIndex u ntc) (getIndex v ntc) 
   705              in 
   706 	      if uvfound then (
   707 	       let 
   708 	        val (xufound, xupred) = dfs (op =) sccGraph xi (getIndex u ntc)
   709 	       in
   710 		if xufound then (
   711 		 let 
   712 		  val (vyfound, vypred) =  dfs (op =) sccGraph (getIndex v ntc) yi
   713 		 in 
   714 		  if vyfound then (
   715 		   let
   716 		    val uvpath = completeComponentPath u v uvpred
   717 		    val uvLesss = mergeLess ( transPath (tl uvpath, hd uvpath), e)
   718 		    val xypath = (completeComponentPath  x u xupred)@[uvLesss]@(completeComponentPath v y vypred)
   719 		    val xyLesss = transPath (tl xypath, hd xypath)
   720 		   in 
   721 		    if xyLesss subsumes subgoal then SOME (getprf xyLesss)
   722                     else NONE
   723 		   end )
   724 		  else NONE   
   725 	         end)
   726 		else NONE
   727 	       end ) 
   728 	      else NONE
   729 	     end )
   730     ) else NONE
   731 end;  
   732    
   733          
   734 in
   735   (* looking for x <= y: any path from x to y is sufficient *)
   736   case subgoal of (Le (x, y, _)) => (
   737   if null sccGraph then raise Cannot else ( 
   738    let 
   739     val xi = getIndex x ntc
   740     val yi = getIndex y ntc
   741     (* searches in sccGraph a path from xi to yi *)
   742     val (found, pred) = dfs (op =) sccGraph xi yi
   743    in 
   744     if found then (
   745        let val xypath = completeComponentPath x y pred 
   746            val xyLesss = transPath (tl xypath, hd xypath) 
   747        in  
   748 	  (case xyLesss of
   749 	    (Less (_, _, q)) => if xyLesss subsumes subgoal then (Thm ([q], Less.less_imp_le))  
   750 				else raise Cannot
   751 	     | _   => if xyLesss subsumes subgoal then (getprf xyLesss) 
   752 	              else raise Cannot)
   753        end )
   754      else raise Cannot 
   755    end 
   756     )
   757    )
   758  (* looking for x < y: particular path required, which is not necessarily
   759     found by normal dfs *)
   760  |   (Less (x, y, _)) => (
   761   if null sccGraph then raise Cannot else (
   762    let 
   763     val xi = getIndex x ntc
   764     val yi = getIndex y ntc
   765     val sccGraph_transpose = transpose (op =) sccGraph
   766     (* all components that can be reached from component xi  *)
   767     val xreachable = dfs_int_reachable sccGraph xi
   768     (* all comonents reachable from y in the transposed graph sccGraph' *)
   769     val yreachable = dfs_int_reachable sccGraph_transpose yi
   770     (* for all edges u ~= v or u < v check if they are part of path x < y *)
   771     fun processNeqEdges [] = raise Cannot 
   772     |   processNeqEdges (e::es) = 
   773       case  (findLess e x y xi yi xreachable yreachable) of (SOME prf) => prf  
   774       | _ => processNeqEdges es
   775         
   776     in 
   777        processNeqEdges neqE 
   778     end
   779   )
   780  )
   781 | (NotEq (x, y, _)) => (
   782   (* if there aren't any edges that are candidate for a ~= raise Cannot *)
   783   if null neqE then raise Cannot
   784   (* if there aren't any edges that are candidate for <= then just search a edge in neqE that implies the subgoal *)
   785   else if null sccSubgraphs then (
   786      (case (Library.find_first (fn fact => fact subsumes subgoal) neqE, subgoal) of
   787        ( SOME (NotEq (x, y, p)), NotEq (x', y', _)) =>
   788           if  (x aconv x' andalso y aconv y') then p 
   789 	  else Thm ([p], Less.not_sym)
   790      | ( SOME (Less (x, y, p)), NotEq (x', y', _)) => 
   791           if x aconv x' andalso y aconv y' then (Thm ([p], Less.less_imp_neq))
   792           else (Thm ([(Thm ([p], Less.less_imp_neq))], Less.not_sym))
   793      | _ => raise Cannot) 
   794    ) else (
   795    
   796    let  val xi = getIndex x ntc 
   797         val yi = getIndex y ntc
   798 	val sccGraph_transpose = transpose (op =) sccGraph
   799         val xreachable = dfs_int_reachable sccGraph xi
   800 	val yreachable = dfs_int_reachable sccGraph_transpose yi
   801 	
   802 	fun processNeqEdges [] = raise Cannot  
   803   	|   processNeqEdges (e::es) = (
   804 	    let val u = lower e 
   805 	        val v = upper e
   806 		val ui = getIndex u ntc
   807 		val vi = getIndex v ntc
   808 		
   809 	    in  
   810 	        (* if x ~= y follows from edge e *)
   811 	    	if e subsumes subgoal then (
   812 		     case e of (Less (u, v, q)) => (
   813 		       if u aconv x andalso v aconv y then (Thm ([q], Less.less_imp_neq))
   814 		       else (Thm ([(Thm ([q], Less.less_imp_neq))], Less.not_sym))
   815 		     )
   816 		     |    (NotEq (u,v, q)) => (
   817 		       if u aconv x andalso v aconv y then q
   818 		       else (Thm ([q],  Less.not_sym))
   819 		     )
   820 		 )
   821                 (* if SCC_x is linked to SCC_y via edge e *)
   822 		 else if ui = xi andalso vi = yi then (
   823                    case e of (Less (_, _,_)) => (
   824 		        let val xypath = (completeTermPath x u (List.nth(sccSubgraphs, ui)) ) @ [e] @ (completeTermPath v y (List.nth(sccSubgraphs, vi)) )
   825 			    val xyLesss = transPath (tl xypath, hd xypath)
   826 			in  (Thm ([getprf xyLesss], Less.less_imp_neq)) end)
   827 		   | _ => (   
   828 		        let 
   829 			    val xupath = completeTermPath x u  (List.nth(sccSubgraphs, ui))
   830 			    val uxpath = completeTermPath u x  (List.nth(sccSubgraphs, ui))
   831 			    val vypath = completeTermPath v y  (List.nth(sccSubgraphs, vi))
   832 			    val yvpath = completeTermPath y v  (List.nth(sccSubgraphs, vi))
   833 			    val xuLesss = transPath (tl xupath, hd xupath)     
   834 			    val uxLesss = transPath (tl uxpath, hd uxpath)			    
   835 			    val vyLesss = transPath (tl vypath, hd vypath)			
   836 			    val yvLesss = transPath (tl yvpath, hd yvpath)
   837 			    val x_eq_u =  (Thm ([(getprf xuLesss),(getprf uxLesss)], Less.eqI))
   838 			    val v_eq_y =  (Thm ([(getprf vyLesss),(getprf yvLesss)], Less.eqI))
   839 			in 
   840                            (Thm ([x_eq_u , (getprf e), v_eq_y ], Less.eq_neq_eq_imp_neq)) 
   841 			end
   842 			)       
   843 		  ) else if ui = yi andalso vi = xi then (
   844 		     case e of (Less (_, _,_)) => (
   845 		        let val xypath = (completeTermPath y u (List.nth(sccSubgraphs, ui)) ) @ [e] @ (completeTermPath v x (List.nth(sccSubgraphs, vi)) )
   846 			    val xyLesss = transPath (tl xypath, hd xypath)
   847 			in (Thm ([(Thm ([getprf xyLesss], Less.less_imp_neq))] , Less.not_sym)) end ) 
   848 		     | _ => (
   849 		        
   850 			let val yupath = completeTermPath y u (List.nth(sccSubgraphs, ui))
   851 			    val uypath = completeTermPath u y (List.nth(sccSubgraphs, ui))
   852 			    val vxpath = completeTermPath v x (List.nth(sccSubgraphs, vi))
   853 			    val xvpath = completeTermPath x v (List.nth(sccSubgraphs, vi))
   854 			    val yuLesss = transPath (tl yupath, hd yupath)     
   855 			    val uyLesss = transPath (tl uypath, hd uypath)			    
   856 			    val vxLesss = transPath (tl vxpath, hd vxpath)			
   857 			    val xvLesss = transPath (tl xvpath, hd xvpath)
   858 			    val y_eq_u =  (Thm ([(getprf yuLesss),(getprf uyLesss)], Less.eqI))
   859 			    val v_eq_x =  (Thm ([(getprf vxLesss),(getprf xvLesss)], Less.eqI))
   860 			in
   861 			    (Thm ([(Thm ([y_eq_u , (getprf e), v_eq_x ], Less.eq_neq_eq_imp_neq))], Less.not_sym))
   862 		        end
   863 		       )
   864 		  ) else (
   865                        (* there exists a path x < y or y < x such that
   866                           x ~= y may be concluded *)
   867 	        	case  (findLess e x y xi yi xreachable yreachable) of 
   868 		              (SOME prf) =>  (Thm ([prf], Less.less_imp_neq))  
   869                              | NONE =>  (
   870 		               let 
   871 		                val yr = dfs_int_reachable sccGraph yi
   872 	                        val xr = dfs_int_reachable sccGraph_transpose xi
   873 		               in 
   874 		                case  (findLess e y x yi xi yr xr) of 
   875 		                      (SOME prf) => (Thm ([(Thm ([prf], Less.less_imp_neq))], Less.not_sym)) 
   876                                       | _ => processNeqEdges es
   877 		               end)
   878 		 ) end) 
   879      in processNeqEdges neqE end)
   880   )    
   881 end;
   882 
   883 
   884 (* ******************************************************************* *)
   885 (*                                                                     *)
   886 (* mk_sccGraphs components leqG neqG ntc :                             *)
   887 (* Term.term list list ->                                              *)
   888 (* (Term.term * (Term.term * less) list) list ->                       *)
   889 (* (Term.term * (Term.term * less) list) list ->                       *)
   890 (* (Term.term * int)  list ->                                          *)
   891 (* (int * (int * less) list) list   *                                  *)
   892 (* ((Term.term * (Term.term * less) list) list) list                   *)
   893 (*                                                                     *)
   894 (*                                                                     *)
   895 (* Computes, from graph leqG, list of all its components and the list  *)
   896 (* ntc (nodes, index of component) a graph whose nodes are the         *)
   897 (* indices of the components of g.  Egdes of the new graph are         *)
   898 (* only the edges of g linking two components. Also computes for each  *)
   899 (* component the subgraph of leqG that forms this component.           *)
   900 (*                                                                     *)
   901 (* For each component SCC_i is checked if there exists a edge in neqG  *)
   902 (* that leads to a contradiction.                                      *)
   903 (*                                                                     *)
   904 (* We have a contradiction for edge u ~= v and u < v if:               *)
   905 (* - u and v are in the same component,                                *)
   906 (* that is, a path u <= v and a path v <= u exist, hence u = v.        *)
   907 (* From irreflexivity of < follows u < u or v < v. Ex false quodlibet. *)
   908 (*                                                                     *)
   909 (* ******************************************************************* *)
   910 
   911 fun mk_sccGraphs _ [] _ _ = ([],[])
   912 |   mk_sccGraphs components leqG neqG ntc = 
   913     let
   914     (* Liste (Index der Komponente, Komponente *)
   915     val IndexComp = indexComps components;
   916 
   917        
   918     fun handleContr edge g = 
   919        (case edge of 
   920           (Less  (x, y, _)) => (
   921 	    let 
   922 	     val xxpath = edge :: (completeTermPath y x g )
   923 	     val xxLesss = transPath (tl xxpath, hd xxpath)
   924 	     val q = getprf xxLesss
   925 	    in 
   926 	     raise (Contr (Thm ([q], Less.less_reflE ))) 
   927 	    end 
   928 	  )
   929         | (NotEq (x, y, _)) => (
   930 	    let 
   931 	     val xypath = (completeTermPath x y g )
   932 	     val yxpath = (completeTermPath y x g )
   933 	     val xyLesss = transPath (tl xypath, hd xypath)
   934 	     val yxLesss = transPath (tl yxpath, hd yxpath)
   935              val q = getprf (mergeLess ((mergeLess (edge, xyLesss)),yxLesss )) 
   936 	    in 
   937 	     raise (Contr (Thm ([q], Less.less_reflE )))
   938 	    end  
   939 	 )
   940 	| _ =>  error "trans_tac/handleContr: invalid Contradiction");
   941  
   942    	
   943     (* k is index of the actual component *)   
   944        
   945     fun processComponent (k, comp) = 
   946      let    
   947         (* all edges with weight <= of the actual component *)  
   948         val leqEdges = List.concat (map (adjacent (op aconv) leqG) comp);
   949         (* all edges with weight ~= of the actual component *)  
   950         val neqEdges = map snd (List.concat (map (adjacent (op aconv) neqG) comp));
   951 
   952        (* find an edge leading to a contradiction *)   
   953        fun findContr [] = NONE
   954        |   findContr (e::es) = 
   955 		    let val ui = (getIndex (lower e) ntc) 
   956 			val vi = (getIndex (upper e) ntc) 
   957 		    in 
   958 		        if ui = vi then  SOME e
   959 		        else findContr es
   960 		    end; 
   961 		   
   962 		(* sort edges into component internal edges and 
   963 		   edges pointing away from the component *)
   964 		fun sortEdges  [] (intern,extern)  = (intern,extern)
   965 		|   sortEdges  ((v,l)::es) (intern, extern) = 
   966 		    let val k' = getIndex v ntc in 
   967 		        if k' = k then 
   968 			    sortEdges es (l::intern, extern)
   969 			else sortEdges  es (intern, (k',l)::extern) end;
   970 		
   971 		(* Insert edge into sorted list of edges, where edge is
   972                     only added if
   973                     - it is found for the first time
   974                     - it is a <= edge and no parallel < edge was found earlier
   975                     - it is a < edge
   976                  *)
   977           	 fun insert (h,l) [] = [(h,l)]
   978 		 |   insert (h,l) ((k',l')::es) = if h = k' then (
   979 		     case l of (Less (_, _, _)) => (h,l)::es
   980 		     | _  => (case l' of (Less (_, _, _)) => (h,l')::es
   981 	                      | _ => (k',l)::es) )
   982 		     else (k',l'):: insert (h,l) es;
   983 		
   984 		(* Reorganise list of edges such that
   985                     - duplicate edges are removed
   986                     - if a < edge and a <= edge exist at the same time,
   987                       remove <= edge *)
   988     		 fun reOrganizeEdges [] sorted = sorted: (int * less) list
   989 		 |   reOrganizeEdges (e::es) sorted = reOrganizeEdges es (insert e sorted); 
   990 	
   991                  (* construct the subgraph forming the strongly connected component
   992 		    from the edge list *)    
   993 		 fun sccSubGraph [] g  = g
   994 		 |   sccSubGraph (l::ls) g = 
   995 		          sccSubGraph ls (addEdge ((lower l),[((upper l),l)],g))
   996 		 
   997 		 val (intern, extern) = sortEdges leqEdges ([], []);
   998                  val subGraph = sccSubGraph intern [];
   999 		  
  1000      in  
  1001          case findContr neqEdges of SOME e => handleContr e subGraph
  1002 	 | _ => ((k, (reOrganizeEdges (extern) [])), subGraph)
  1003      end; 
  1004   
  1005     val tmp =  map processComponent IndexComp    
  1006 in 
  1007      ( (map fst tmp), (map snd tmp))  
  1008 end; 
  1009 
  1010 (* *********************************************************************** *)
  1011 (*                                                                         *)
  1012 (* solvePartialOrder sign (asms,concl) :                                   *)
  1013 (* theory -> less list * Term.term -> proof list                           *)
  1014 (*                                                                         *)
  1015 (* Find proof if possible for partial orders.                              *)
  1016 (*                                                                         *)
  1017 (* *********************************************************************** *)
  1018 
  1019 fun solvePartialOrder sign (asms, concl) =
  1020  let 
  1021   val (leqG, neqG, neqE) = mkGraphs asms
  1022   val components = scc_term leqG
  1023   val ntc = indexNodes (indexComps components)
  1024   val (sccGraph, sccSubgraphs) = mk_sccGraphs components leqG neqG ntc 
  1025  in
  1026    let 
  1027    val (subgoals, prf) = mkconcl_partial sign concl
  1028    fun solve facts less =
  1029        (case triv_solv less of NONE => findProof (sccGraph, neqE, ntc, sccSubgraphs ) less
  1030        | SOME prf => prf )
  1031   in
  1032    map (solve asms) subgoals
  1033   end
  1034  end;
  1035 
  1036 (* *********************************************************************** *)
  1037 (*                                                                         *)
  1038 (* solveTotalOrder sign (asms,concl) :                                     *)
  1039 (* theory -> less list * Term.term -> proof list                           *)
  1040 (*                                                                         *)
  1041 (* Find proof if possible for linear orders.                               *)
  1042 (*                                                                         *)
  1043 (* *********************************************************************** *)
  1044 
  1045 fun solveTotalOrder sign (asms, concl) =
  1046  let 
  1047   val (leqG, neqG, neqE) = mkGraphs asms
  1048   val components = scc_term leqG   
  1049   val ntc = indexNodes (indexComps components)
  1050   val (sccGraph, sccSubgraphs) = mk_sccGraphs components leqG neqG ntc
  1051  in
  1052    let 
  1053    val (subgoals, prf) = mkconcl_linear sign concl
  1054    fun solve facts less =
  1055       (case triv_solv less of NONE => findProof (sccGraph, neqE, ntc, sccSubgraphs) less
  1056       | SOME prf => prf )
  1057   in
  1058    map (solve asms) subgoals
  1059   end
  1060  end;
  1061   
  1062 (* partial_tac - solves partial orders *)
  1063 val partial_tac = SUBGOAL (fn (A, n, sign) =>
  1064  let
  1065   val rfrees = map Free (rename_wrt_term A (Logic.strip_params A))
  1066   val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
  1067   val C = subst_bounds (rfrees, Logic.strip_assums_concl A)
  1068   val lesss = List.concat (ListPair.map (mkasm_partial sign) (Hs, 0 upto (length Hs - 1)))
  1069   val prfs = solvePartialOrder sign (lesss, C);
  1070   val (subgoals, prf) = mkconcl_partial sign C;
  1071  in
  1072   METAHYPS (fn asms =>
  1073     let val thms = map (prove asms) prfs
  1074     in rtac (prove thms prf) 1 end) n
  1075  end
  1076  handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n
  1077       | Cannot  => no_tac
  1078       );
  1079        
  1080 (* linear_tac - solves linear/total orders *)
  1081 val linear_tac = SUBGOAL (fn (A, n, sign) =>
  1082  let
  1083   val rfrees = map Free (rename_wrt_term A (Logic.strip_params A))
  1084   val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
  1085   val C = subst_bounds (rfrees, Logic.strip_assums_concl A)
  1086   val lesss = List.concat (ListPair.map (mkasm_linear sign) (Hs, 0 upto (length Hs - 1)))
  1087   val prfs = solveTotalOrder sign (lesss, C);
  1088   val (subgoals, prf) = mkconcl_linear sign C;
  1089  in
  1090   METAHYPS (fn asms =>
  1091     let val thms = map (prove asms) prfs
  1092     in rtac (prove thms prf) 1 end) n
  1093  end
  1094  handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n
  1095       | Cannot  => no_tac);
  1096        
  1097 end;