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