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.8 +   Copyright:	TU Muenchen
     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.293 +    else (u,dl):: (addEdge(v,d,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.314 +           buildGraphs (ls, addEdge(y,[],(addEdge (x,[(y,leEdge)],leG))), neqEdges@neqE) 
   1.315 +	 end
   1.316 +     |  (Le (x,y,p))   => buildGraphs (ls, addEdge(y,[],(addEdge (x,[(y,l)],leG))), neqE) 
   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.344 +fun adjacent eq_comp ((v,adj)::el) u = 
   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;