# HG changeset patch # User ballarin # Date 1091434600 -7200 # Node ID 0726e7b156185750abc08f7339ded4205ff611cd # Parent b807858b97bddaa6cf6206ab833ba5714b3828c4 Documentation added/improved. diff -r b807858b97bd -r 0726e7b15618 src/Provers/order.ML --- a/src/Provers/order.ML Mon Aug 02 10:15:37 2004 +0200 +++ b/src/Provers/order.ML Mon Aug 02 10:16:40 2004 +0200 @@ -38,10 +38,10 @@ val eqI: thm (* [| x <= y; y <= x |] ==> x = y *) val eqD1: thm (* x = y ==> x <= y *) val eqD2: thm (* x = y ==> y <= x *) - val less_trans: thm (* [| x <= y; y <= z |] ==> x <= z *) - val less_le_trans: thm (* [| x <= y; y < z |] ==> x < z *) - val le_less_trans: thm (* [| x < y; y <= z |] ==> x < z *) - val le_trans: thm (* [| x < y; y < z |] ==> x < z *) + val less_trans: thm (* [| x < y; y < z |] ==> x < z *) + val less_le_trans: thm (* [| x < y; y <= z |] ==> x < z *) + val le_less_trans: thm (* [| x <= y; y < z |] ==> x < z *) + val le_trans: thm (* [| x <= y; y <= z |] ==> x <= z *) val le_neq_trans : thm (* [| x <= y ; x ~= y |] ==> x < y *) val neq_le_trans : thm (* [| x ~= y ; x <= y |] ==> x < y *) @@ -56,7 +56,8 @@ val eq_neq_eq_imp_neq : thm (* [| x = u ; u ~= v ; v = z|] ==> x ~= z *) (* Analysis of premises and conclusion *) - (* decomp_x (`x Rel y') should yield (x, Rel, y) + (* decomp_part is for partial_tac, decomp_lin is for linear_tac; + decomp_x (`x Rel y') should yield (x, Rel, y) where Rel is one of "<", "<=", "~<", "~<=", "=" and "~=", other relation symbols cause an error message *) val decomp_part: Sign.sg -> term -> (term * string * term) option diff -r b807858b97bd -r 0726e7b15618 src/Provers/trancl.ML --- a/src/Provers/trancl.ML Mon Aug 02 10:15:37 2004 +0200 +++ b/src/Provers/trancl.ML Mon Aug 02 10:16:40 2004 +0200 @@ -1,10 +1,33 @@ (* - Title: Transitivity reasoner for partial and linear orders + Title: Transitivity reasoner for transitive closures of relations Id: $Id$ Author: Oliver Kutter Copyright: TU Muenchen *) +(* + +The packages provides tactics trancl_tac and rtrancl_tac that prove +goals of the form + + (x,y) : r^+ and (x,y) : r^* (rtrancl_tac only) + +from premises of the form + + (x,y) : r, (x,y) : r^+ and (x,y) : r^* (rtrancl_tac only) + +by reflexivity and transitivity. The relation r is determined by inspecting +the conclusion. + +The package is implemented as an ML functor and thus not limited to +particular constructs for transitive and reflexive-transitive +closures, neither need relations be represented as sets of pairs. In +order to instantiate the package for transitive closure only, supply +dummy theorems to the additional rules for reflexive-transitive +closures, and don't use rtrancl_tac! + +*) + signature TRANCL_ARITH = sig @@ -30,6 +53,20 @@ val rtrancl_trans : thm (* [| (a,b) : r^* ; (b,c) : r^* |] ==> (a,c) : r^* *) + (* decomp: decompose a premise or conclusion + + Returns one of the following: + + None if not an instance of a relation, + Some (x, y, r, s) if instance of a relation, where + x: left hand side argument, y: right hand side argument, + r: the relation, + s: the kind of closure, one of + "r": the relation itself, + "r^+": transitive closure of the relation, + "r^*": reflexive-transitive closure of the relation + *) + val decomp: term -> (term * term * term * string) option end; @@ -48,7 +85,7 @@ = Asm of int | Thm of proof list * thm; - exception Cannot; + exception Cannot; (* internal exception: raised if no proof can be found *) fun prove asms = let fun pr (Asm i) = nth_elem (i, asms) @@ -58,23 +95,30 @@ (* Internal datatype for inequalities *) datatype rel - = R of term * term * proof (* just a unknown relation R *) - | Trans of term * term * proof (* R^+ *) + = Trans of term * term * proof (* R^+ *) | RTrans of term * term * proof; (* R^* *) (* Misc functions for datatype rel *) -fun lower (R (x, _, _)) = x - | lower (Trans (x, _, _)) = x +fun lower (Trans (x, _, _)) = x | lower (RTrans (x,_,_)) = x; -fun upper (R (_, y, _)) = y - | upper (Trans (_, y, _)) = y +fun upper (Trans (_, y, _)) = y | upper (RTrans (_,y,_)) = y; -fun getprf (R (_, _, p)) = p -| getprf (Trans (_, _, p)) = p +fun getprf (Trans (_, _, p)) = p | getprf (RTrans (_,_, p)) = p; +(* ************************************************************************ *) +(* *) +(* mkasm_trancl Rel (t,n): term -> (term , int) -> rel list *) +(* *) +(* Analyse assumption t with index n with respect to relation Rel: *) +(* If t is of the form "(x, y) : Rel" (or Rel^+), translate to *) +(* an object (singleton list) of internal datatype rel. *) +(* Otherwise return empty list. *) +(* *) +(* ************************************************************************ *) + fun mkasm_trancl Rel (t, n) = case Cls.decomp t of Some (x, y, rel,r) => if rel aconv Rel then @@ -87,6 +131,17 @@ else [] | None => []; +(* ************************************************************************ *) +(* *) +(* mkasm_rtrancl Rel (t,n): term -> (term , int) -> rel list *) +(* *) +(* Analyse assumption t with index n with respect to relation Rel: *) +(* If t is of the form "(x, y) : Rel" (or Rel^+ or Rel^* ), translate to *) +(* an object (singleton list) of internal datatype rel. *) +(* Otherwise return empty list. *) +(* *) +(* ************************************************************************ *) + fun mkasm_rtrancl Rel (t, n) = case Cls.decomp t of Some (x, y, rel, r) => if rel aconv Rel then @@ -98,6 +153,19 @@ else [] | None => []; +(* ************************************************************************ *) +(* *) +(* mkconcl_trancl t: term -> (term, rel, proof) *) +(* mkconcl_rtrancl t: term -> (term, rel, proof) *) +(* *) +(* Analyse conclusion t: *) +(* - must be of form "(x, y) : r^+ (or r^* for rtrancl) *) +(* - returns r *) +(* - conclusion in internal form *) +(* - proof object *) +(* *) +(* ************************************************************************ *) + fun mkconcl_trancl t = case Cls.decomp t of Some (x, y, rel, r) => (case r of @@ -113,13 +181,25 @@ | _ => raise Cannot) | None => raise Cannot; -(* trans. cls. rules *) +(* ************************************************************************ *) +(* *) +(* makeStep (r1, r2): rel * rel -> rel *) +(* *) +(* Apply transitivity to r1 and r2, obtaining a new element of r^+ or r^*, *) +(* according the following rules: *) +(* *) +(* ( (a, b) : r^+ , (b,c) : r^+ ) --> (a,c) : r^+ *) +(* ( (a, b) : r^* , (b,c) : r^+ ) --> (a,c) : r^+ *) +(* ( (a, b) : r^+ , (b,c) : r^* ) --> (a,c) : r^+ *) +(* ( (a, b) : r^* , (b,c) : r^* ) --> (a,c) : r^* *) +(* *) +(* ************************************************************************ *) + fun makeStep (Trans (a,_,p), Trans(_,c,q)) = Trans (a,c, Thm ([p,q], Cls.trancl_trans)) (* refl. + trans. cls. rules *) | makeStep (RTrans (a,_,p), Trans(_,c,q)) = Trans (a,c, Thm ([p,q], Cls.rtrancl_trancl_trancl)) | makeStep (Trans (a,_,p), RTrans(_,c,q)) = Trans (a,c, Thm ([p,q], Cls.trancl_rtrancl_trancl)) -| makeStep (RTrans (a,_,p), RTrans(_,c,q)) = RTrans (a,c, Thm ([p,q], Cls.rtrancl_trans)) -| makeStep (a,b) = error ("trancl_tac: internal error in makeStep: undefined case"); +| makeStep (RTrans (a,_,p), RTrans(_,c,q)) = RTrans (a,c, Thm ([p,q], Cls.rtrancl_trans)); (* ******************************************************************* *) (* *) @@ -150,6 +230,7 @@ (* ********************************************************************** *) (* *) (* mkGraph constructs from a list of objects of type rel a graph g *) +(* and a list of all edges with label r+. *) (* *) (* ********************************************************************** *) @@ -295,7 +376,7 @@ (* (bool, rel list) *) (* *) (* Searches a path from vertex x to vertex y in Graph g, returns true and *) -(* the list of edges of edges if path is found, otherwise false and nil. *) +(* the list of edges if path is found, otherwise false and nil. *) (* *) (* ************************************************************************ *) @@ -330,9 +411,16 @@ end; +(* ************************************************************************ *) +(* *) +(* findRtranclProof g tranclEdges subgoal: *) +(* (Term.term * (Term.term * rel list) list) -> rel -> proof list *) +(* *) +(* Searches in graph g a proof for subgoal. *) +(* *) +(* ************************************************************************ *) fun findRtranclProof g tranclEdges subgoal = - (* simple case first *) case subgoal of (RTrans (x,y,_)) => if x aconv y then [Thm ([], Cls.rtrancl_refl)] else ( let val (found, path) = findPath (lower subgoal) (upper subgoal) g in @@ -424,16 +512,11 @@ let val (_, subgoal, _) = mkconcl_trancl concl val (found, path) = findPath (lower subgoal) (upper subgoal) g in - - if found then [getprf (transPath (tl path, hd path))] else raise Cannot - end end; - - fun solveRtrancl (asms, concl) = let val (g,tranclEdges) = mkGraph asms val (_, subgoal, _) = mkconcl_rtrancl concl @@ -475,4 +558,3 @@ handle Cannot => no_tac); end; -