src/Provers/quasi.ML
author wenzelm
Thu Dec 07 00:42:04 2006 +0100 (2006-12-07)
changeset 21687 f689f729afab
parent 19250 932a50e2332f
child 22578 b0eb5652f210
permissions -rw-r--r--
reorganized structure Goal vs. Tactic;
     1 (* 
     2    Title:	Reasoner for simple transitivity and quasi orders. 
     3    Id:		$Id$
     4    Author:	Oliver Kutter
     5    Copyright:	TU Muenchen
     6  *)
     7 
     8 (* 
     9  
    10 The package provides tactics trans_tac and quasi_tac that use
    11 premises of the form 
    12 
    13   t = u, t ~= u, t < u and t <= u
    14 
    15 to
    16 - either derive a contradiction, in which case the conclusion can be
    17   any term,
    18 - or prove the concluson, which must be of the form t ~= u, t < u or
    19   t <= u.
    20 
    21 Details:
    22 
    23 1. trans_tac:
    24    Only premises of form t <= u are used and the conclusion must be of
    25    the same form.  The conclusion is proved, if possible, by a chain of
    26    transitivity from the assumptions.
    27 
    28 2. quasi_tac:
    29    <= is assumed to be a quasi order and < its strict relative, defined
    30    as t < u == t <= u & t ~= u.  Again, the conclusion is proved from
    31    the assumptions.
    32    Note that the presence of a strict relation is not necessary for
    33    quasi_tac.  Configure decomp_quasi to ignore < and ~=.  A list of
    34    required theorems for both situations is given below. 
    35 *)
    36 
    37 signature LESS_ARITH =
    38 sig
    39   (* Transitivity of <=
    40      Note that transitivities for < hold for partial orders only. *) 
    41   val le_trans: thm  (* [| x <= y; y <= z |] ==> x <= z *)
    42  
    43   (* Additional theorem for quasi orders *)
    44   val le_refl: thm  (* x <= x *)
    45   val eqD1: thm (* x = y ==> x <= y *)
    46   val eqD2: thm (* x = y ==> y <= x *)
    47 
    48   (* Additional theorems for premises of the form x < y *)
    49   val less_reflE: thm  (* x < x ==> P *)
    50   val less_imp_le : thm (* x < y ==> x <= y *)
    51 
    52   (* Additional theorems for premises of the form x ~= y *)
    53   val le_neq_trans : thm (* [| x <= y ; x ~= y |] ==> x < y *)
    54   val neq_le_trans : thm (* [| x ~= y ; x <= y |] ==> x < y *)
    55 
    56   (* Additional theorem for goals of form x ~= y *)
    57   val less_imp_neq : thm (* x < y ==> x ~= y *)
    58 
    59   (* Analysis of premises and conclusion *)
    60   (* decomp_x (`x Rel y') should yield SOME (x, Rel, y)
    61        where Rel is one of "<", "<=", "=" and "~=",
    62        other relation symbols cause an error message *)
    63   (* decomp_trans is used by trans_tac, it may only return Rel = "<=" *)
    64   val decomp_trans: theory -> term -> (term * string * term) option
    65   (* decomp_quasi is used by quasi_tac *)
    66   val decomp_quasi: theory -> term -> (term * string * term) option
    67 end;
    68 
    69 signature QUASI_TAC = 
    70 sig
    71   val trans_tac: int -> tactic
    72   val quasi_tac: int -> tactic
    73 end;
    74 
    75 functor Quasi_Tac_Fun (Less: LESS_ARITH): QUASI_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, sign_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_trans 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 (* Only assumptions of form x <= y are used, all others are ignored         *)
   125 (*                                                                          *)
   126 (* ************************************************************************ *)
   127 
   128 fun mkasm_trans sign (t, n) =
   129   case Less.decomp_trans sign t of
   130     SOME (x, rel, y) => 
   131     (case rel of
   132      "<="  =>  [Le (x, y, Asm n)]
   133     | _     => error ("trans_tac: unknown relation symbol ``" ^ rel ^
   134                  "''returned by decomp_trans."))
   135   | NONE => [];
   136   
   137 (* ************************************************************************ *)
   138 (*                                                                          *)
   139 (* mkasm_quasi sign (t, n) : theory -> (Term.term * int) -> less            *)
   140 (*                                                                          *)
   141 (* Tuple (t, n) (t an assumption, n its index in the assumptions) is        *)
   142 (* translated to an element of type less.                                   *)
   143 (* Quasi orders only.                                                       *)
   144 (*                                                                          *)
   145 (* ************************************************************************ *)
   146 
   147 fun mkasm_quasi sign (t, n) =
   148   case Less.decomp_quasi sign t of
   149     SOME (x, rel, y) => (case rel of
   150       "<"   => if (x aconv y) then raise Contr (Thm ([Asm n], Less.less_reflE)) 
   151                else [Less (x, y, Asm n)]
   152     | "<="  => [Le (x, y, Asm n)]
   153     | "="   => [Le (x, y, Thm ([Asm n], Less.eqD1)),
   154                 Le (y, x, Thm ([Asm n], Less.eqD2))]
   155     | "~="  => if (x aconv y) then 
   156                   raise Contr (Thm ([(Thm ([(Thm ([], Less.le_refl)) ,(Asm n)], Less.le_neq_trans))], Less.less_reflE))
   157                else [ NotEq (x, y, Asm n),
   158                       NotEq (y, x,Thm ( [Asm n], thm "not_sym"))] 
   159     | _     => error ("quasi_tac: unknown relation symbol ``" ^ rel ^
   160                  "''returned by decomp_quasi."))
   161   | NONE => [];
   162 
   163 
   164 (* ************************************************************************ *)
   165 (*                                                                          *)
   166 (* mkconcl_trans sign t : theory -> Term.term -> less                       *)
   167 (*                                                                          *)
   168 (* Translates conclusion t to an element of type less.                      *)
   169 (* Only for Conclusions of form x <= y or x < y.                            *)
   170 (*                                                                          *)
   171 (* ************************************************************************ *)
   172 
   173   
   174 fun mkconcl_trans sign t =
   175   case Less.decomp_trans sign t of
   176     SOME (x, rel, y) => (case rel of
   177      "<="  => (Le (x, y, Asm ~1), Asm 0) 
   178     | _  => raise Cannot)
   179   | NONE => raise Cannot;
   180   
   181   
   182 (* ************************************************************************ *)
   183 (*                                                                          *)
   184 (* mkconcl_quasi sign t : theory -> Term.term -> less                       *)
   185 (*                                                                          *)
   186 (* Translates conclusion t to an element of type less.                      *)
   187 (* Quasi orders only.                                                       *)
   188 (*                                                                          *)
   189 (* ************************************************************************ *)
   190 
   191 fun mkconcl_quasi sign t =
   192   case Less.decomp_quasi sign t of
   193     SOME (x, rel, y) => (case rel of
   194       "<"   => ([Less (x, y, Asm ~1)], Asm 0)
   195     | "<="  => ([Le (x, y, Asm ~1)], Asm 0)
   196     | "~="  => ([NotEq (x,y, Asm ~1)], Asm 0)
   197     | _  => raise Cannot)
   198 | NONE => raise Cannot;
   199   
   200   
   201 (* ******************************************************************* *)
   202 (*                                                                     *)
   203 (* mergeLess (less1,less2):  less * less -> less                       *)
   204 (*                                                                     *)
   205 (* Merge to elements of type less according to the following rules     *)
   206 (*                                                                     *)
   207 (* x <= y && y <= z ==> x <= z                                         *)
   208 (* x <= y && x ~= y ==> x < y                                          *)
   209 (* x ~= y && x <= y ==> x < y                                          *)
   210 (*                                                                     *)
   211 (* ******************************************************************* *)
   212 
   213 fun mergeLess (Le (x, _, p) , Le (_ , z, q)) =
   214       Le (x, z, Thm ([p,q] , Less.le_trans))
   215 |   mergeLess (Le (x, z, p) , NotEq (x', z', q)) =
   216       if (x aconv x' andalso z aconv z' ) 
   217        then Less (x, z, Thm ([p,q] , Less.le_neq_trans))
   218         else error "quasi_tac: internal error le_neq_trans"
   219 |   mergeLess (NotEq (x, z, p) , Le (x' , z', q)) =
   220       if (x aconv x' andalso z aconv z') 
   221       then Less (x, z, Thm ([p,q] , Less.neq_le_trans))
   222       else error "quasi_tac: internal error neq_le_trans"
   223 |   mergeLess (_, _) =
   224       error "quasi_tac: internal error: undefined case";
   225 
   226 
   227 (* ******************************************************************** *)
   228 (* tr checks for valid transitivity step                                *)
   229 (* ******************************************************************** *)
   230 
   231 infix tr;
   232 fun (Le (_, y, _))   tr (Le (x', _, _))   = ( y aconv x' )
   233   | _ tr _ = false;
   234   
   235 (* ******************************************************************* *)
   236 (*                                                                     *)
   237 (* transPath (Lesslist, Less): (less list * less) -> less              *)
   238 (*                                                                     *)
   239 (* If a path represented by a list of elements of type less is found,  *)
   240 (* this needs to be contracted to a single element of type less.       *)
   241 (* Prior to each transitivity step it is checked whether the step is   *)
   242 (* valid.                                                              *)
   243 (*                                                                     *)
   244 (* ******************************************************************* *)
   245 
   246 fun transPath ([],lesss) = lesss
   247 |   transPath (x::xs,lesss) =
   248       if lesss tr x then transPath (xs, mergeLess(lesss,x))
   249       else error "trans/quasi_tac: internal error transpath";
   250   
   251 (* ******************************************************************* *)
   252 (*                                                                     *)
   253 (* less1 subsumes less2 : less -> less -> bool                         *)
   254 (*                                                                     *)
   255 (* subsumes checks whether less1 implies less2                         *)
   256 (*                                                                     *)
   257 (* ******************************************************************* *)
   258   
   259 infix subsumes;
   260 fun (Le (x, y, _)) subsumes (Le (x', y', _)) =
   261       (x aconv x' andalso y aconv y')
   262   | (Le _) subsumes (Less _) =
   263       error "trans/quasi_tac: internal error: Le cannot subsume Less"
   264   | (NotEq(x,y,_)) subsumes (NotEq(x',y',_)) = x aconv x' andalso y aconv y' orelse x aconv y' andalso y aconv x'
   265   | _ subsumes _ = false;
   266 
   267 (* ******************************************************************* *)
   268 (*                                                                     *)
   269 (* triv_solv less1 : less ->  proof option                     *)
   270 (*                                                                     *)
   271 (* Solves trivial goal x <= x.                                         *)
   272 (*                                                                     *)
   273 (* ******************************************************************* *)
   274 
   275 fun triv_solv (Le (x, x', _)) =
   276     if x aconv x' then  SOME (Thm ([], Less.le_refl)) 
   277     else NONE
   278 |   triv_solv _ = NONE;
   279 
   280 (* ********************************************************************* *)
   281 (* Graph functions                                                       *)
   282 (* ********************************************************************* *)
   283 
   284 (* *********************************************************** *)
   285 (* Functions for constructing graphs                           *)
   286 (* *********************************************************** *)
   287 
   288 fun addEdge (v,d,[]) = [(v,d)]
   289 |   addEdge (v,d,((u,dl)::el)) = if v aconv u then ((v,d@dl)::el)
   290     else (u,dl):: (addEdge(v,d,el));
   291     
   292 (* ********************************************************************** *)
   293 (*                                                                        *)
   294 (* mkQuasiGraph constructs from a list of objects of type less a graph g, *) 
   295 (* by taking all edges that are candidate for a <=, and a list neqE, by   *)
   296 (* taking all edges that are candiate for a ~=                            *)
   297 (*                                                                        *)
   298 (* ********************************************************************** *)
   299 
   300 fun mkQuasiGraph [] = ([],[])
   301 |   mkQuasiGraph lessList = 
   302  let
   303  fun buildGraphs ([],leG, neqE) = (leG,  neqE)
   304   |   buildGraphs (l::ls, leG,  neqE) = case l of 
   305        (Less (x,y,p)) =>
   306          let 
   307 	  val leEdge  = Le (x,y, Thm ([p], Less.less_imp_le)) 
   308 	  val neqEdges = [ NotEq (x,y, Thm ([p], Less.less_imp_neq)),
   309 	                   NotEq (y,x, Thm ( [Thm ([p], Less.less_imp_neq)], thm "not_sym"))]
   310 	 in
   311            buildGraphs (ls, addEdge(y,[],(addEdge (x,[(y,leEdge)],leG))), neqEdges@neqE) 
   312 	 end
   313      |  (Le (x,y,p))   => buildGraphs (ls, addEdge(y,[],(addEdge (x,[(y,l)],leG))), neqE) 
   314      | _ =>  buildGraphs (ls, leG,  l::neqE) ;
   315 
   316 in buildGraphs (lessList, [],  []) end;
   317   
   318 (* ********************************************************************** *)
   319 (*                                                                        *)
   320 (* mkGraph constructs from a list of objects of type less a graph g       *)
   321 (* Used for plain transitivity chain reasoning.                           *)
   322 (*                                                                        *)
   323 (* ********************************************************************** *)
   324 
   325 fun mkGraph [] = []
   326 |   mkGraph lessList = 
   327  let
   328   fun buildGraph ([],g) = g
   329   |   buildGraph (l::ls, g) =  buildGraph (ls, (addEdge ((lower l),[((upper l),l)],g))) 
   330      
   331 in buildGraph (lessList, []) end;
   332 
   333 (* *********************************************************************** *)
   334 (*                                                                         *)
   335 (* adjacent g u : (''a * 'b list ) list -> ''a -> 'b list                  *)
   336 (*                                                                         *)
   337 (* List of successors of u in graph g                                      *)
   338 (*                                                                         *)
   339 (* *********************************************************************** *)
   340  
   341 fun adjacent eq_comp ((v,adj)::el) u = 
   342     if eq_comp (u, v) then adj else adjacent eq_comp el u
   343 |   adjacent _  []  _ = []  
   344 
   345 (* *********************************************************************** *)
   346 (*                                                                         *)
   347 (* dfs eq_comp g u v:                                                      *)
   348 (* ('a * 'a -> bool) -> ('a  *( 'a * less) list) list ->                   *)
   349 (* 'a -> 'a -> (bool * ('a * less) list)                                   *) 
   350 (*                                                                         *)
   351 (* Depth first search of v from u.                                         *)
   352 (* Returns (true, path(u, v)) if successful, otherwise (false, []).        *)
   353 (*                                                                         *)
   354 (* *********************************************************************** *)
   355 
   356 fun dfs eq_comp g u v = 
   357  let 
   358     val pred = ref nil;
   359     val visited = ref nil;
   360     
   361     fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
   362     
   363     fun dfs_visit u' = 
   364     let val _ = visited := u' :: (!visited)
   365     
   366     fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end;
   367     
   368     in if been_visited v then () 
   369     else (app (fn (v',l) => if been_visited v' then () else (
   370        update (v',l); 
   371        dfs_visit v'; ()) )) (adjacent eq_comp g u')
   372      end
   373   in 
   374     dfs_visit u; 
   375     if (been_visited v) then (true, (!pred)) else (false , [])   
   376   end;
   377 
   378 (* ************************************************************************ *)
   379 (*                                                                          *)
   380 (* Begin: Quasi Order relevant functions                                    *)
   381 (*                                                                          *)
   382 (*                                                                          *)
   383 (* ************************************************************************ *)
   384 
   385 (* ************************************************************************ *)
   386 (*                                                                          *)
   387 (* findPath x y g: Term.term -> Term.term ->                                *)
   388 (*                  (Term.term * (Term.term * less list) list) ->           *)
   389 (*                  (bool, less list)                                       *)
   390 (*                                                                          *)
   391 (*  Searches a path from vertex x to vertex y in Graph g, returns true and  *)
   392 (*  the list of edges forming the path, if a path is found, otherwise false *)
   393 (*  and nil.                                                                *)
   394 (*                                                                          *)
   395 (* ************************************************************************ *)
   396 
   397 
   398  fun findPath x y g = 
   399   let 
   400     val (found, tmp) =  dfs (op aconv) g x y ;
   401     val pred = map snd tmp;
   402 
   403     fun path x y  =
   404       let
   405        (* find predecessor u of node v and the edge u -> v *)
   406        fun lookup v [] = raise Cannot
   407        |   lookup v (e::es) = if (upper e) aconv v then e else lookup v es;
   408 		
   409        (* traverse path backwards and return list of visited edges *)   
   410        fun rev_path v = 
   411  	let val l = lookup v pred
   412             val u = lower l;
   413  	in
   414            if u aconv x then [l] else (rev_path u) @ [l] 
   415 	end
   416       in rev_path y end;
   417 		
   418   in 
   419    if found then (
   420     if x aconv y then (found,[(Le (x, y, (Thm ([], Less.le_refl))))])
   421     else (found, (path x y) )) 
   422    else (found,[])
   423   end; 
   424 	
   425       
   426 (* ************************************************************************ *) 
   427 (*                                                                          *)
   428 (* findQuasiProof (leqG, neqE) subgoal:                                     *)
   429 (* (Term.term * (Term.term * less list) list) * less list  -> less -> proof *)
   430 (*                                                                          *)
   431 (* Constructs a proof for subgoal by searching a special path in leqG and   *)
   432 (* neqE. Raises Cannot if construction of the proof fails.                  *)   
   433 (*                                                                          *)
   434 (* ************************************************************************ *) 
   435 
   436 
   437 (* As the conlusion can be either of form x <= y, x < y or x ~= y we have        *)
   438 (* three cases to deal with. Finding a transitivity path from x to y with label  *)
   439 (* 1. <=                                                                         *) 
   440 (*    This is simply done by searching any path from x to y in the graph leG.    *)
   441 (*    The graph leG contains only edges with label <=.                           *)
   442 (*                                                                               *)
   443 (* 2. <                                                                          *)
   444 (*    A path from x to y with label < can be found by searching a path with      *)
   445 (*    label <= from x to y in the graph leG and merging the path x <= y with     *)
   446 (*    a parallel edge x ~= y resp. y ~= x to x < y.                              *)
   447 (*                                                                               *)
   448 (* 3. ~=                                                                         *)
   449 (*   If the conclusion is of form x ~= y, we can find a proof either directly,   *)
   450 (*   if x ~= y or y ~= x are among the assumptions, or by constructing x ~= y if *)
   451 (*   x < y or y < x follows from the assumptions.                                *)
   452 
   453 fun findQuasiProof (leG, neqE) subgoal =
   454   case subgoal of (Le (x,y, _)) => (
   455    let 
   456     val (xyLefound,xyLePath) = findPath x y leG 
   457    in
   458     if xyLefound then (
   459      let 
   460       val Le_x_y = (transPath (tl xyLePath, hd xyLePath))
   461      in getprf Le_x_y end )
   462     else raise Cannot
   463    end )
   464   | (Less (x,y,_))  => (
   465    let 
   466     fun findParallelNeq []  = NONE
   467     |   findParallelNeq (e::es)  =
   468      if      (x aconv (lower e) andalso y aconv (upper e)) then SOME e
   469      else if (y aconv (lower e) andalso x aconv (upper e)) then SOME (NotEq (x,y, (Thm ([getprf e], thm "not_sym"))))
   470      else findParallelNeq es ;  
   471    in
   472    (* test if there is a edge x ~= y respectivly  y ~= x and     *)
   473    (* if it possible to find a path x <= y in leG, thus we can conclude x < y *)
   474     (case findParallelNeq neqE of (SOME e) => 
   475       let 
   476        val (xyLeFound,xyLePath) = findPath x y leG 
   477       in
   478        if xyLeFound then (
   479         let 
   480          val Le_x_y = (transPath (tl xyLePath, hd xyLePath))
   481          val Less_x_y = mergeLess (e, Le_x_y)
   482         in getprf Less_x_y end
   483        ) else raise Cannot
   484       end 
   485     | _ => raise Cannot)    
   486    end )
   487  | (NotEq (x,y,_)) => 
   488   (* First check if a single premiss is sufficient *)
   489   (case (Library.find_first (fn fact => fact subsumes subgoal) neqE, subgoal) of
   490     (SOME (NotEq (x, y, p)), NotEq (x', y', _)) =>
   491       if  (x aconv x' andalso y aconv y') then p 
   492       else Thm ([p], thm "not_sym")
   493     | _  => raise Cannot 
   494   )
   495 
   496       
   497 (* ************************************************************************ *) 
   498 (*                                                                          *) 
   499 (* End: Quasi Order relevant functions                                      *) 
   500 (*                                                                          *) 
   501 (*                                                                          *) 
   502 (* ************************************************************************ *) 
   503 
   504 (* *********************************************************************** *)
   505 (*                                                                         *)
   506 (* solveLeTrans sign (asms,concl) :                                        *)
   507 (* theory -> less list * Term.term -> proof list                           *)
   508 (*                                                                         *)
   509 (* Solves                                                                  *)
   510 (*                                                                         *)
   511 (* *********************************************************************** *)
   512 
   513 fun solveLeTrans sign (asms, concl) =
   514  let 
   515   val g = mkGraph asms
   516  in
   517    let 
   518     val (subgoal, prf) = mkconcl_trans sign concl
   519     val (found, path) = findPath (lower subgoal) (upper subgoal) g 
   520    in
   521     if found then [getprf (transPath (tl path, hd path))] 
   522     else raise Cannot
   523   end
   524  end;
   525 
   526 
   527 (* *********************************************************************** *)
   528 (*                                                                         *)
   529 (* solveQuasiOrder sign (asms,concl) :                                     *)
   530 (* theory -> less list * Term.term -> proof list                           *)
   531 (*                                                                         *)
   532 (* Find proof if possible for quasi order.                                 *)
   533 (*                                                                         *)
   534 (* *********************************************************************** *)
   535 
   536 fun solveQuasiOrder sign (asms, concl) =
   537  let 
   538   val (leG, neqE) = mkQuasiGraph asms
   539  in
   540    let 
   541    val (subgoals, prf) = mkconcl_quasi sign concl
   542    fun solve facts less =
   543        (case triv_solv less of NONE => findQuasiProof (leG, neqE) less
   544        | SOME prf => prf )
   545   in   map (solve asms) subgoals end
   546  end;
   547 
   548 (* ************************************************************************ *) 
   549 (*                                                                          *) 
   550 (* Tactics                                                                  *)
   551 (*                                                                          *)
   552 (*  - trans_tac                                                          *)                     
   553 (*  - quasi_tac, solves quasi orders                                        *)                     
   554 (* ************************************************************************ *) 
   555 
   556 
   557 (* trans_tac - solves transitivity chains over <= *)
   558 val trans_tac  =  SUBGOAL (fn (A, n, sign) =>
   559  let
   560   val rfrees = map Free (rename_wrt_term A (Logic.strip_params A))
   561   val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
   562   val C = subst_bounds (rfrees, Logic.strip_assums_concl A)
   563   val lesss = List.concat (ListPair.map (mkasm_trans  sign) (Hs, 0 upto (length Hs - 1)))
   564   val prfs = solveLeTrans  sign (lesss, C);
   565   
   566   val (subgoal, prf) = mkconcl_trans  sign C;
   567  in
   568   
   569   METAHYPS (fn asms =>
   570     let val thms = map (prove asms) prfs
   571     in rtac (prove thms prf) 1 end) n
   572   
   573  end
   574  handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n
   575       | Cannot  => no_tac
   576 );
   577 
   578 (* quasi_tac - solves quasi orders *)
   579 val quasi_tac = SUBGOAL (fn (A, n, sign) =>
   580  let
   581   val rfrees = map Free (rename_wrt_term A (Logic.strip_params A))
   582   val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
   583   val C = subst_bounds (rfrees, Logic.strip_assums_concl A)
   584   val lesss = List.concat (ListPair.map (mkasm_quasi sign) (Hs, 0 upto (length Hs - 1)))
   585   val prfs = solveQuasiOrder sign (lesss, C);
   586   val (subgoals, prf) = mkconcl_quasi sign C;
   587  in
   588  
   589   METAHYPS (fn asms =>
   590     let val thms = map (prove asms) prfs
   591     in rtac (prove thms prf) 1 end) n
   592  
   593  end
   594  handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n
   595       | Cannot  => no_tac
   596 );
   597    
   598 end;