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;
```