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