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 *)
8 (* TODO: reduce number of input thms *)
10 (*
12 The package provides tactics partial_tac and linear_tac that use all
13 premises of the form
15   t = u, t ~= u, t < u, t <= u, ~(t < u) and ~(t <= u)
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)
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!
30 *)
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 *)
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) *)
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 *)
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;
69 signature ORDER_TAC  =
70 sig
71   val partial_tac: int -> tactic
72   val linear_tac:  int -> tactic
73 end;
75 functor Order_Tac_Fun (Less: LESS_ARITH): ORDER_TAC =
76 struct
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;
83 (* Internal datatype for the proof *)
84 datatype proof
85   = Asm of int
86   | Thm of proof list * thm;
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 *)
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;
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;
105 (* Misc functions for datatype less *)
106 fun lower (Less (x, _, _)) = x
107   | lower (Le (x, _, _)) = x
108   | lower (NotEq (x,_,_)) = x;
110 fun upper (Less (_, y, _)) = y
111   | upper (Le (_, y, _)) = y
112   | upper (NotEq (_,y,_)) = y;
114 fun getprf   (Less (_, _, p)) = p
115 |   getprf   (Le   (_, _, p)) = p
116 |   getprf   (NotEq (_,_, p)) = p;
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 (* ************************************************************************ *)
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 => [];
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 (* ************************************************************************ *)
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 => [];
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 (* ************************************************************************ *)
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;
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 (* ************************************************************************ *)
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;
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 (* ******************************************************************* *)
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";
263 (* ******************************************************************** *)
264 (* tr checks for valid transitivity step                                *)
265 (* ******************************************************************** *)
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;
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 (* ******************************************************************* *)
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";
291 (* ******************************************************************* *)
292 (*                                                                     *)
293 (* less1 subsumes less2 : less -> less -> bool                         *)
294 (*                                                                     *)
295 (* subsumes checks whether less1 implies less2                         *)
296 (*                                                                     *)
297 (* ******************************************************************* *)
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;
314 (* ******************************************************************* *)
315 (*                                                                     *)
316 (* triv_solv less1 : less ->  proof option                     *)
317 (*                                                                     *)
318 (* Solves trivial goal x <= x.                                         *)
319 (*                                                                     *)
320 (* ******************************************************************* *)
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;
327 (* ********************************************************************* *)
328 (* Graph functions                                                       *)
329 (* ********************************************************************* *)
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 (* ******************************************************************* *)
357 (* *********************************************************** *)
358 (* Functions for constructing graphs                           *)
359 (* *********************************************************** *)
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));
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 (* ********************************************************************* *)
373 fun mkGraphs [] = ([],[],[])
374 |   mkGraphs lessList =
375  let
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) ;
387   in buildGraphs (lessList, [], [], []) end;
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 (* *********************************************************************** *)
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 _  []  _ = []
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 (* *********************************************************************** *)
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
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)
428     end
429    | gather (_,nil) = (nil,nil)
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
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)
443  in assemble g flipped end
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 (* *********************************************************************** *)
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
464   (* List of vertices which have been visited. *)
465   val visited : term list ref = ref nil
467   fun been_visited v = exists (fn w => w aconv v) (!visited)
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)
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
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;
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). *)
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;
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 (* *********************************************************************** *)
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
523   fun been_visited v = exists (fn w => w = v) (!visited)
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
534  in u :: dfs_visit g u end;
537 fun indexComps components =
538     ListPair.map (fn (a,b) => (a,b)) (0 upto (length components -1), components);
540 fun indexNodes IndexComp =
541     List.concat (map (fn (index, comp) => (map (fn v => (v,index)) comp)) IndexComp);
543 fun getIndex v [] = ~1
544 |   getIndex v ((v',k)::vs) = if v aconv v' then k else getIndex v vs;
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 (* *********************************************************************** *)
559 fun dfs eq_comp g u v =
560  let
561     val pred = ref nil;
562     val visited = ref nil;
564     fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
566     fun dfs_visit u' =
567     let val _ = visited := u' :: (!visited)
569     fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end;
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;
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 (* *********************************************************************** *)
596 fun completeTermPath u v g  =
597   let
598    val (found, tmp) =  dfs (op aconv) g u v ;
599    val pred = map snd tmp;
601    fun path x y  =
602       let
604       (* find predecessor u of node v and the edge u -> v *)
606       fun lookup v [] = raise Cannot
607       |   lookup v (e::es) = if (upper e) aconv v then e else lookup v es;
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;
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;
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 (* *********************************************************************** *)
637 fun findProof (sccGraph, neqE, ntc, sccSubgraphs) subgoal =
638 let
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
646 	  fun lookup k [] =  raise Cannot
647 	  |   lookup k ((h,l)::us) = if k = h then l else lookup k us;
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;
667 (* ******************************************************************* *)
668 (* findLess e x y xi yi xreachable yreachable                          *)
669 (*                                                                     *)
670 (* Find a path from x through e to y, of weight <                      *)
671 (* ******************************************************************* *)
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
679   in
680       if ui mem xreachable andalso vi mem xreachable andalso
681          ui mem yreachable andalso vi mem yreachable then (
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;
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
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 (
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
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
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 		     | _ => (
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;
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 (* ******************************************************************* *)
911 fun mk_sccGraphs _ [] _ _ = ([],[])
912 |   mk_sccGraphs components leqG neqG ntc =
913     let
914     (* Liste (Index der Komponente, Komponente *)
915     val IndexComp = indexComps components;
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");
943     (* k is index of the actual component *)
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));
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;
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;
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;
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);
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))
997 		 val (intern, extern) = sortEdges leqEdges ([], []);
998                  val subGraph = sccSubGraph intern [];
1000      in
1001          case findContr neqEdges of SOME e => handleContr e subGraph
1002 	 | _ => ((k, (reOrganizeEdges (extern) [])), subGraph)
1003      end;
1005     val tmp =  map processComponent IndexComp
1006 in
1007      ( (map fst tmp), (map snd tmp))
1008 end;
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 (* *********************************************************************** *)
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;
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 (* *********************************************************************** *)
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;
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       );
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);
1097 end;