src/Provers/quasi.ML
 changeset 15103 79846e8792eb child 15531 08c8dad8e399
```     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Provers/quasi.ML	Tue Aug 03 14:47:51 2004 +0200
1.3 @@ -0,0 +1,598 @@
1.4 +(*
1.5 +   Title:	Reasoner for simple transitivity and quasi orders.
1.6 +   Id:		\$Id\$
1.7 +   Author:	Oliver Kutter
1.9 + *)
1.10 +
1.11 +(*
1.12 +
1.13 +The package provides tactics trans_tac and quasi_tac that use
1.14 +premises of the form
1.15 +
1.16 +  t = u, t ~= u, t < u and t <= u
1.17 +
1.18 +to
1.19 +- either derive a contradiction, in which case the conclusion can be
1.20 +  any term,
1.21 +- or prove the concluson, which must be of the form t ~= u, t < u or
1.22 +  t <= u.
1.23 +
1.24 +Details:
1.25 +
1.26 +1. trans_tac:
1.27 +   Only premises of form t <= u are used and the conclusion must be of
1.28 +   the same form.  The conclusion is proved, if possible, by a chain of
1.29 +   transitivity from the assumptions.
1.30 +
1.31 +2. quasi_tac:
1.32 +   <= is assumed to be a quasi order and < its strict relative, defined
1.33 +   as t < u == t <= u & t ~= u.  Again, the conclusion is proved from
1.34 +   the assumptions.
1.35 +   Note that the presence of a strict relation is not necessary for
1.36 +   quasi_tac.  Configure decomp_quasi to ignore < and ~=.  A list of
1.37 +   required theorems for both situations is given below.
1.38 +*)
1.39 +
1.40 +signature LESS_ARITH =
1.41 +sig
1.42 +  (* Transitivity of <=
1.43 +     Note that transitivities for < hold for partial orders only. *)
1.44 +  val le_trans: thm  (* [| x <= y; y <= z |] ==> x <= z *)
1.45 +
1.46 +  (* Additional theorem for quasi orders *)
1.47 +  val le_refl: thm  (* x <= x *)
1.48 +  val eqD1: thm (* x = y ==> x <= y *)
1.49 +  val eqD2: thm (* x = y ==> y <= x *)
1.50 +
1.51 +  (* Additional theorems for premises of the form x < y *)
1.52 +  val less_reflE: thm  (* x < x ==> P *)
1.53 +  val less_imp_le : thm (* x < y ==> x <= y *)
1.54 +
1.55 +  (* Additional theorems for premises of the form x ~= y *)
1.56 +  val le_neq_trans : thm (* [| x <= y ; x ~= y |] ==> x < y *)
1.57 +  val neq_le_trans : thm (* [| x ~= y ; x <= y |] ==> x < y *)
1.58 +
1.59 +  (* Additional theorem for goals of form x ~= y *)
1.60 +  val less_imp_neq : thm (* x < y ==> x ~= y *)
1.61 +
1.62 +  (* Analysis of premises and conclusion *)
1.63 +  (* decomp_x (`x Rel y') should yield Some (x, Rel, y)
1.64 +       where Rel is one of "<", "<=", "=" and "~=",
1.65 +       other relation symbols cause an error message *)
1.66 +  (* decomp_trans is used by trans_tac, it may only return Rel = "<=" *)
1.67 +  val decomp_trans: Sign.sg -> term -> (term * string * term) option
1.68 +  (* decomp_quasi is used by quasi_tac *)
1.69 +  val decomp_quasi: Sign.sg -> term -> (term * string * term) option
1.70 +end;
1.71 +
1.72 +signature QUASI_TAC =
1.73 +sig
1.74 +  val trans_tac: int -> tactic
1.75 +  val quasi_tac: int -> tactic
1.76 +end;
1.77 +
1.78 +functor Quasi_Tac_Fun (Less: LESS_ARITH): QUASI_TAC =
1.79 +struct
1.80 +
1.81 +(* Extract subgoal with signature *)
1.82 +fun SUBGOAL goalfun i st =
1.83 +  goalfun (List.nth(prems_of st, i-1),  i, sign_of_thm st) st
1.84 +                             handle Subscript => Seq.empty;
1.85 +
1.86 +(* Internal datatype for the proof *)
1.87 +datatype proof
1.88 +  = Asm of int
1.89 +  | Thm of proof list * thm;
1.90 +
1.91 +exception Cannot;
1.92 + (* Internal exception, raised if conclusion cannot be derived from
1.93 +     assumptions. *)
1.94 +exception Contr of proof;
1.95 +  (* Internal exception, raised if contradiction ( x < x ) was derived *)
1.96 +
1.97 +fun prove asms =
1.98 +  let fun pr (Asm i) = nth_elem (i, asms)
1.99 +  |       pr (Thm (prfs, thm)) = (map pr prfs) MRS thm
1.100 +  in pr end;
1.101 +
1.102 +(* Internal datatype for inequalities *)
1.103 +datatype less
1.104 +   = Less  of term * term * proof
1.105 +   | Le    of term * term * proof
1.106 +   | NotEq of term * term * proof;
1.107 +
1.108 + (* Misc functions for datatype less *)
1.109 +fun lower (Less (x, _, _)) = x
1.110 +  | lower (Le (x, _, _)) = x
1.111 +  | lower (NotEq (x,_,_)) = x;
1.112 +
1.113 +fun upper (Less (_, y, _)) = y
1.114 +  | upper (Le (_, y, _)) = y
1.115 +  | upper (NotEq (_,y,_)) = y;
1.116 +
1.117 +fun getprf   (Less (_, _, p)) = p
1.118 +|   getprf   (Le   (_, _, p)) = p
1.119 +|   getprf   (NotEq (_,_, p)) = p;
1.120 +
1.121 +(* ************************************************************************ *)
1.122 +(*                                                                          *)
1.123 +(* mkasm_trans sign (t, n) :  Sign.sg -> (Term.term * int)  -> less         *)
1.124 +(*                                                                          *)
1.125 +(* Tuple (t, n) (t an assumption, n its index in the assumptions) is        *)
1.126 +(* translated to an element of type less.                                   *)
1.127 +(* Only assumptions of form x <= y are used, all others are ignored         *)
1.128 +(*                                                                          *)
1.129 +(* ************************************************************************ *)
1.130 +
1.131 +fun mkasm_trans sign (t, n) =
1.132 +  case Less.decomp_trans sign t of
1.133 +    Some (x, rel, y) =>
1.134 +    (case rel of
1.135 +     "<="  =>  [Le (x, y, Asm n)]
1.136 +    | _     => error ("trans_tac: unknown relation symbol ``" ^ rel ^
1.137 +                 "''returned by decomp_trans."))
1.138 +  | None => [];
1.139 +
1.140 +(* ************************************************************************ *)
1.141 +(*                                                                          *)
1.142 +(* mkasm_quasi sign (t, n) : Sign.sg -> (Term.term * int) -> less           *)
1.143 +(*                                                                          *)
1.144 +(* Tuple (t, n) (t an assumption, n its index in the assumptions) is        *)
1.145 +(* translated to an element of type less.                                   *)
1.146 +(* Quasi orders only.                                                       *)
1.147 +(*                                                                          *)
1.148 +(* ************************************************************************ *)
1.149 +
1.150 +fun mkasm_quasi sign (t, n) =
1.151 +  case Less.decomp_quasi sign t of
1.152 +    Some (x, rel, y) => (case rel of
1.153 +      "<"   => if (x aconv y) then raise Contr (Thm ([Asm n], Less.less_reflE))
1.154 +               else [Less (x, y, Asm n)]
1.155 +    | "<="  => [Le (x, y, Asm n)]
1.156 +    | "="   => [Le (x, y, Thm ([Asm n], Less.eqD1)),
1.157 +                Le (y, x, Thm ([Asm n], Less.eqD2))]
1.158 +    | "~="  => if (x aconv y) then
1.159 +                  raise Contr (Thm ([(Thm ([(Thm ([], Less.le_refl)) ,(Asm n)], Less.le_neq_trans))], Less.less_reflE))
1.160 +               else [ NotEq (x, y, Asm n),
1.161 +                      NotEq (y, x,Thm ( [Asm n], thm "not_sym"))]
1.162 +    | _     => error ("quasi_tac: unknown relation symbol ``" ^ rel ^
1.163 +                 "''returned by decomp_quasi."))
1.164 +  | None => [];
1.165 +
1.166 +
1.167 +(* ************************************************************************ *)
1.168 +(*                                                                          *)
1.169 +(* mkconcl_trans sign t : Sign.sg -> Term.term -> less                      *)
1.170 +(*                                                                          *)
1.171 +(* Translates conclusion t to an element of type less.                      *)
1.172 +(* Only for Conclusions of form x <= y or x < y.                            *)
1.173 +(*                                                                          *)
1.174 +(* ************************************************************************ *)
1.175 +
1.176 +
1.177 +fun mkconcl_trans sign t =
1.178 +  case Less.decomp_trans sign t of
1.179 +    Some (x, rel, y) => (case rel of
1.180 +     "<="  => (Le (x, y, Asm ~1), Asm 0)
1.181 +    | _  => raise Cannot)
1.182 +  | None => raise Cannot;
1.183 +
1.184 +
1.185 +(* ************************************************************************ *)
1.186 +(*                                                                          *)
1.187 +(* mkconcl_quasi sign t : Sign.sg -> Term.term -> less                      *)
1.188 +(*                                                                          *)
1.189 +(* Translates conclusion t to an element of type less.                      *)
1.190 +(* Quasi orders only.                                                       *)
1.191 +(*                                                                          *)
1.192 +(* ************************************************************************ *)
1.193 +
1.194 +fun mkconcl_quasi sign t =
1.195 +  case Less.decomp_quasi sign t of
1.196 +    Some (x, rel, y) => (case rel of
1.197 +      "<"   => ([Less (x, y, Asm ~1)], Asm 0)
1.198 +    | "<="  => ([Le (x, y, Asm ~1)], Asm 0)
1.199 +    | "~="  => ([NotEq (x,y, Asm ~1)], Asm 0)
1.200 +    | _  => raise Cannot)
1.201 +| None => raise Cannot;
1.202 +
1.203 +
1.204 +(* ******************************************************************* *)
1.205 +(*                                                                     *)
1.206 +(* mergeLess (less1,less2):  less * less -> less                       *)
1.207 +(*                                                                     *)
1.208 +(* Merge to elements of type less according to the following rules     *)
1.209 +(*                                                                     *)
1.210 +(* x <= y && y <= z ==> x <= z                                         *)
1.211 +(* x <= y && x ~= y ==> x < y                                          *)
1.212 +(* x ~= y && x <= y ==> x < y                                          *)
1.213 +(*                                                                     *)
1.214 +(* ******************************************************************* *)
1.215 +
1.216 +fun mergeLess (Le (x, _, p) , Le (_ , z, q)) =
1.217 +      Le (x, z, Thm ([p,q] , Less.le_trans))
1.218 +|   mergeLess (Le (x, z, p) , NotEq (x', z', q)) =
1.219 +      if (x aconv x' andalso z aconv z' )
1.220 +       then Less (x, z, Thm ([p,q] , Less.le_neq_trans))
1.221 +        else error "quasi_tac: internal error le_neq_trans"
1.222 +|   mergeLess (NotEq (x, z, p) , Le (x' , z', q)) =
1.223 +      if (x aconv x' andalso z aconv z')
1.224 +      then Less (x, z, Thm ([p,q] , Less.neq_le_trans))
1.225 +      else error "quasi_tac: internal error neq_le_trans"
1.226 +|   mergeLess (_, _) =
1.227 +      error "quasi_tac: internal error: undefined case";
1.228 +
1.229 +
1.230 +(* ******************************************************************** *)
1.231 +(* tr checks for valid transitivity step                                *)
1.232 +(* ******************************************************************** *)
1.233 +
1.234 +infix tr;
1.235 +fun (Le (_, y, _))   tr (Le (x', _, _))   = ( y aconv x' )
1.236 +  | _ tr _ = false;
1.237 +
1.238 +(* ******************************************************************* *)
1.239 +(*                                                                     *)
1.240 +(* transPath (Lesslist, Less): (less list * less) -> less              *)
1.241 +(*                                                                     *)
1.242 +(* If a path represented by a list of elements of type less is found,  *)
1.243 +(* this needs to be contracted to a single element of type less.       *)
1.244 +(* Prior to each transitivity step it is checked whether the step is   *)
1.245 +(* valid.                                                              *)
1.246 +(*                                                                     *)
1.247 +(* ******************************************************************* *)
1.248 +
1.249 +fun transPath ([],lesss) = lesss
1.250 +|   transPath (x::xs,lesss) =
1.251 +      if lesss tr x then transPath (xs, mergeLess(lesss,x))
1.252 +      else error "trans/quasi_tac: internal error transpath";
1.253 +
1.254 +(* ******************************************************************* *)
1.255 +(*                                                                     *)
1.256 +(* less1 subsumes less2 : less -> less -> bool                         *)
1.257 +(*                                                                     *)
1.258 +(* subsumes checks whether less1 implies less2                         *)
1.259 +(*                                                                     *)
1.260 +(* ******************************************************************* *)
1.261 +
1.262 +infix subsumes;
1.263 +fun (Le (x, y, _)) subsumes (Le (x', y', _)) =
1.264 +      (x aconv x' andalso y aconv y')
1.265 +  | (Le _) subsumes (Less _) =
1.266 +      error "trans/quasi_tac: internal error: Le cannot subsume Less"
1.267 +  | (NotEq(x,y,_)) subsumes (NotEq(x',y',_)) = x aconv x' andalso y aconv y' orelse x aconv y' andalso y aconv x'
1.268 +  | _ subsumes _ = false;
1.269 +
1.270 +(* ******************************************************************* *)
1.271 +(*                                                                     *)
1.272 +(* triv_solv less1 : less ->  proof Library.option                     *)
1.273 +(*                                                                     *)
1.274 +(* Solves trivial goal x <= x.                                         *)
1.275 +(*                                                                     *)
1.276 +(* ******************************************************************* *)
1.277 +
1.278 +fun triv_solv (Le (x, x', _)) =
1.279 +    if x aconv x' then  Some (Thm ([], Less.le_refl))
1.280 +    else None
1.281 +|   triv_solv _ = None;
1.282 +
1.283 +(* ********************************************************************* *)
1.284 +(* Graph functions                                                       *)
1.285 +(* ********************************************************************* *)
1.286 +
1.287 +(* *********************************************************** *)
1.288 +(* Functions for constructing graphs                           *)
1.289 +(* *********************************************************** *)
1.290 +
1.291 +fun addEdge (v,d,[]) = [(v,d)]
1.292 +|   addEdge (v,d,((u,dl)::el)) = if v aconv u then ((v,d@dl)::el)
1.294 +
1.295 +(* ********************************************************************** *)
1.296 +(*                                                                        *)
1.297 +(* mkQuasiGraph constructs from a list of objects of type less a graph g, *)
1.298 +(* by taking all edges that are candidate for a <=, and a list neqE, by   *)
1.299 +(* taking all edges that are candiate for a ~=                            *)
1.300 +(*                                                                        *)
1.301 +(* ********************************************************************** *)
1.302 +
1.303 +fun mkQuasiGraph [] = ([],[])
1.304 +|   mkQuasiGraph lessList =
1.305 + let
1.306 + fun buildGraphs ([],leG, neqE) = (leG,  neqE)
1.307 +  |   buildGraphs (l::ls, leG,  neqE) = case l of
1.308 +       (Less (x,y,p)) =>
1.309 +         let
1.310 +	  val leEdge  = Le (x,y, Thm ([p], Less.less_imp_le))
1.311 +	  val neqEdges = [ NotEq (x,y, Thm ([p], Less.less_imp_neq)),
1.312 +	                   NotEq (y,x, Thm ( [Thm ([p], Less.less_imp_neq)], thm "not_sym"))]
1.313 +	 in
1.315 +	 end
1.317 +     | _ =>  buildGraphs (ls, leG,  l::neqE) ;
1.318 +
1.319 +in buildGraphs (lessList, [],  []) end;
1.320 +
1.321 +(* ********************************************************************** *)
1.322 +(*                                                                        *)
1.323 +(* mkGraph constructs from a list of objects of type less a graph g       *)
1.324 +(* Used for plain transitivity chain reasoning.                           *)
1.325 +(*                                                                        *)
1.326 +(* ********************************************************************** *)
1.327 +
1.328 +fun mkGraph [] = []
1.329 +|   mkGraph lessList =
1.330 + let
1.331 +  fun buildGraph ([],g) = g
1.332 +  |   buildGraph (l::ls, g) =  buildGraph (ls, (addEdge ((lower l),[((upper l),l)],g)))
1.333 +
1.334 +in buildGraph (lessList, []) end;
1.335 +
1.336 +(* *********************************************************************** *)
1.337 +(*                                                                         *)
1.338 +(* adjacent g u : (''a * 'b list ) list -> ''a -> 'b list                  *)
1.339 +(*                                                                         *)
1.340 +(* List of successors of u in graph g                                      *)
1.341 +(*                                                                         *)
1.342 +(* *********************************************************************** *)
1.343 +
1.345 +    if eq_comp (u, v) then adj else adjacent eq_comp el u
1.346 +|   adjacent _  []  _ = []
1.347 +
1.348 +(* *********************************************************************** *)
1.349 +(*                                                                         *)
1.350 +(* dfs eq_comp g u v:                                                      *)
1.351 +(* ('a * 'a -> bool) -> ('a  *( 'a * less) list) list ->                   *)
1.352 +(* 'a -> 'a -> (bool * ('a * less) list)                                   *)
1.353 +(*                                                                         *)
1.354 +(* Depth first search of v from u.                                         *)
1.355 +(* Returns (true, path(u, v)) if successful, otherwise (false, []).        *)
1.356 +(*                                                                         *)
1.357 +(* *********************************************************************** *)
1.358 +
1.359 +fun dfs eq_comp g u v =
1.360 + let
1.361 +    val pred = ref nil;
1.362 +    val visited = ref nil;
1.363 +
1.364 +    fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
1.365 +
1.366 +    fun dfs_visit u' =
1.367 +    let val _ = visited := u' :: (!visited)
1.368 +
1.369 +    fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end;
1.370 +
1.371 +    in if been_visited v then ()
1.372 +    else (app (fn (v',l) => if been_visited v' then () else (
1.373 +       update (v',l);
1.374 +       dfs_visit v'; ()) )) (adjacent eq_comp g u')
1.375 +     end
1.376 +  in
1.377 +    dfs_visit u;
1.378 +    if (been_visited v) then (true, (!pred)) else (false , [])
1.379 +  end;
1.380 +
1.381 +(* ************************************************************************ *)
1.382 +(*                                                                          *)
1.383 +(* Begin: Quasi Order relevant functions                                    *)
1.384 +(*                                                                          *)
1.385 +(*                                                                          *)
1.386 +(* ************************************************************************ *)
1.387 +
1.388 +(* ************************************************************************ *)
1.389 +(*                                                                          *)
1.390 +(* findPath x y g: Term.term -> Term.term ->                                *)
1.391 +(*                  (Term.term * (Term.term * less list) list) ->           *)
1.392 +(*                  (bool, less list)                                       *)
1.393 +(*                                                                          *)
1.394 +(*  Searches a path from vertex x to vertex y in Graph g, returns true and  *)
1.395 +(*  the list of edges forming the path, if a path is found, otherwise false *)
1.396 +(*  and nil.                                                                *)
1.397 +(*                                                                          *)
1.398 +(* ************************************************************************ *)
1.399 +
1.400 +
1.401 + fun findPath x y g =
1.402 +  let
1.403 +    val (found, tmp) =  dfs (op aconv) g x y ;
1.404 +    val pred = map snd tmp;
1.405 +
1.406 +    fun path x y  =
1.407 +      let
1.408 +       (* find predecessor u of node v and the edge u -> v *)
1.409 +       fun lookup v [] = raise Cannot
1.410 +       |   lookup v (e::es) = if (upper e) aconv v then e else lookup v es;
1.411 +
1.412 +       (* traverse path backwards and return list of visited edges *)
1.413 +       fun rev_path v =
1.414 + 	let val l = lookup v pred
1.415 +            val u = lower l;
1.416 + 	in
1.417 +           if u aconv x then [l] else (rev_path u) @ [l]
1.418 +	end
1.419 +      in rev_path y end;
1.420 +
1.421 +  in
1.422 +   if found then (
1.423 +    if x aconv y then (found,[(Le (x, y, (Thm ([], Less.le_refl))))])
1.424 +    else (found, (path x y) ))
1.425 +   else (found,[])
1.426 +  end;
1.427 +
1.428 +
1.429 +(* ************************************************************************ *)
1.430 +(*                                                                          *)
1.431 +(* findQuasiProof (leqG, neqE) subgoal:                                     *)
1.432 +(* (Term.term * (Term.term * less list) list) * less list  -> less -> proof *)
1.433 +(*                                                                          *)
1.434 +(* Constructs a proof for subgoal by searching a special path in leqG and   *)
1.435 +(* neqE. Raises Cannot if construction of the proof fails.                  *)
1.436 +(*                                                                          *)
1.437 +(* ************************************************************************ *)
1.438 +
1.439 +
1.440 +(* As the conlusion can be either of form x <= y, x < y or x ~= y we have        *)
1.441 +(* three cases to deal with. Finding a transitivity path from x to y with label  *)
1.442 +(* 1. <=                                                                         *)
1.443 +(*    This is simply done by searching any path from x to y in the graph leG.    *)
1.444 +(*    The graph leG contains only edges with label <=.                           *)
1.445 +(*                                                                               *)
1.446 +(* 2. <                                                                          *)
1.447 +(*    A path from x to y with label < can be found by searching a path with      *)
1.448 +(*    label <= from x to y in the graph leG and merging the path x <= y with     *)
1.449 +(*    a parallel edge x ~= y resp. y ~= x to x < y.                              *)
1.450 +(*                                                                               *)
1.451 +(* 3. ~=                                                                         *)
1.452 +(*   If the conclusion is of form x ~= y, we can find a proof either directly,   *)
1.453 +(*   if x ~= y or y ~= x are among the assumptions, or by constructing x ~= y if *)
1.454 +(*   x < y or y < x follows from the assumptions.                                *)
1.455 +
1.456 +fun findQuasiProof (leG, neqE) subgoal =
1.457 +  case subgoal of (Le (x,y, _)) => (
1.458 +   let
1.459 +    val (xyLefound,xyLePath) = findPath x y leG
1.460 +   in
1.461 +    if xyLefound then (
1.462 +     let
1.463 +      val Le_x_y = (transPath (tl xyLePath, hd xyLePath))
1.464 +     in getprf Le_x_y end )
1.465 +    else raise Cannot
1.466 +   end )
1.467 +  | (Less (x,y,_))  => (
1.468 +   let
1.469 +    fun findParallelNeq []  = None
1.470 +    |   findParallelNeq (e::es)  =
1.471 +     if      (x aconv (lower e) andalso y aconv (upper e)) then Some e
1.472 +     else if (y aconv (lower e) andalso x aconv (upper e)) then Some (NotEq (x,y, (Thm ([getprf e], thm "not_sym"))))
1.473 +     else findParallelNeq es ;
1.474 +   in
1.475 +   (* test if there is a edge x ~= y respectivly  y ~= x and     *)
1.476 +   (* if it possible to find a path x <= y in leG, thus we can conclude x < y *)
1.477 +    (case findParallelNeq neqE of (Some e) =>
1.478 +      let
1.479 +       val (xyLeFound,xyLePath) = findPath x y leG
1.480 +      in
1.481 +       if xyLeFound then (
1.482 +        let
1.483 +         val Le_x_y = (transPath (tl xyLePath, hd xyLePath))
1.484 +         val Less_x_y = mergeLess (e, Le_x_y)
1.485 +        in getprf Less_x_y end
1.486 +       ) else raise Cannot
1.487 +      end
1.488 +    | _ => raise Cannot)
1.489 +   end )
1.490 + | (NotEq (x,y,_)) =>
1.491 +  (* First check if a single premiss is sufficient *)
1.492 +  (case (Library.find_first (fn fact => fact subsumes subgoal) neqE, subgoal) of
1.493 +    (Some (NotEq (x, y, p)), NotEq (x', y', _)) =>
1.494 +      if  (x aconv x' andalso y aconv y') then p
1.495 +      else Thm ([p], thm "not_sym")
1.496 +    | _  => raise Cannot
1.497 +  )
1.498 +
1.499 +
1.500 +(* ************************************************************************ *)
1.501 +(*                                                                          *)
1.502 +(* End: Quasi Order relevant functions                                      *)
1.503 +(*                                                                          *)
1.504 +(*                                                                          *)
1.505 +(* ************************************************************************ *)
1.506 +
1.507 +(* *********************************************************************** *)
1.508 +(*                                                                         *)
1.509 +(* solveLeTrans sign (asms,concl) :                                        *)
1.510 +(* Sign.sg -> less list * Term.term -> proof list                          *)
1.511 +(*                                                                         *)
1.512 +(* Solves                                                                  *)
1.513 +(*                                                                         *)
1.514 +(* *********************************************************************** *)
1.515 +
1.516 +fun solveLeTrans sign (asms, concl) =
1.517 + let
1.518 +  val g = mkGraph asms
1.519 + in
1.520 +   let
1.521 +    val (subgoal, prf) = mkconcl_trans sign concl
1.522 +    val (found, path) = findPath (lower subgoal) (upper subgoal) g
1.523 +   in
1.524 +    if found then [getprf (transPath (tl path, hd path))]
1.525 +    else raise Cannot
1.526 +  end
1.527 + end;
1.528 +
1.529 +
1.530 +(* *********************************************************************** *)
1.531 +(*                                                                         *)
1.532 +(* solveQuasiOrder sign (asms,concl) :                                     *)
1.533 +(* Sign.sg -> less list * Term.term -> proof list                          *)
1.534 +(*                                                                         *)
1.535 +(* Find proof if possible for quasi order.                                 *)
1.536 +(*                                                                         *)
1.537 +(* *********************************************************************** *)
1.538 +
1.539 +fun solveQuasiOrder sign (asms, concl) =
1.540 + let
1.541 +  val (leG, neqE) = mkQuasiGraph asms
1.542 + in
1.543 +   let
1.544 +   val (subgoals, prf) = mkconcl_quasi sign concl
1.545 +   fun solve facts less =
1.546 +       (case triv_solv less of None => findQuasiProof (leG, neqE) less
1.547 +       | Some prf => prf )
1.548 +  in   map (solve asms) subgoals end
1.549 + end;
1.550 +
1.551 +(* ************************************************************************ *)
1.552 +(*                                                                          *)
1.553 +(* Tactics                                                                  *)
1.554 +(*                                                                          *)
1.555 +(*  - trans_tac                                                          *)
1.556 +(*  - quasi_tac, solves quasi orders                                        *)
1.557 +(* ************************************************************************ *)
1.558 +
1.559 +
1.560 +(* trans_tac - solves transitivity chains over <= *)
1.561 +val trans_tac  =  SUBGOAL (fn (A, n, sign) =>
1.562 + let
1.563 +  val rfrees = map Free (rename_wrt_term A (Logic.strip_params A))
1.564 +  val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
1.565 +  val C = subst_bounds (rfrees, Logic.strip_assums_concl A)
1.566 +  val lesss = flat (ListPair.map (mkasm_trans  sign) (Hs, 0 upto (length Hs - 1)))
1.567 +  val prfs = solveLeTrans  sign (lesss, C);
1.568 +
1.569 +  val (subgoal, prf) = mkconcl_trans  sign C;
1.570 + in
1.571 +
1.572 +  METAHYPS (fn asms =>
1.573 +    let val thms = map (prove asms) prfs
1.574 +    in rtac (prove thms prf) 1 end) n
1.575 +
1.576 + end
1.577 + handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n
1.578 +      | Cannot  => no_tac
1.579 +);
1.580 +
1.581 +(* quasi_tac - solves quasi orders *)
1.582 +val quasi_tac = SUBGOAL (fn (A, n, sign) =>
1.583 + let
1.584 +  val rfrees = map Free (rename_wrt_term A (Logic.strip_params A))
1.585 +  val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
1.586 +  val C = subst_bounds (rfrees, Logic.strip_assums_concl A)
1.587 +  val lesss = flat (ListPair.map (mkasm_quasi sign) (Hs, 0 upto (length Hs - 1)))
1.588 +  val prfs = solveQuasiOrder sign (lesss, C);
1.589 +  val (subgoals, prf) = mkconcl_quasi sign C;
1.590 + in
1.591 +
1.592 +  METAHYPS (fn asms =>
1.593 +    let val thms = map (prove asms) prfs
1.594 +    in rtac (prove thms prf) 1 end) n
1.595 +
1.596 + end
1.597 + handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n
1.598 +      | Cannot  => no_tac
1.599 +);
1.600 +
1.601 +end;
```