Documentation added/improved.
authorballarin
Mon Aug 02 10:16:40 2004 +0200 (2004-08-02)
changeset 150980726e7b15618
parent 15097 b807858b97bd
child 15099 6d8619440ea0
Documentation added/improved.
src/Provers/order.ML
src/Provers/trancl.ML
     1.1 --- a/src/Provers/order.ML	Mon Aug 02 10:15:37 2004 +0200
     1.2 +++ b/src/Provers/order.ML	Mon Aug 02 10:16:40 2004 +0200
     1.3 @@ -38,10 +38,10 @@
     1.4    val eqI: thm (* [| x <= y; y <= x |] ==> x = y *)
     1.5    val eqD1: thm (* x = y ==> x <= y *)
     1.6    val eqD2: thm (* x = y ==> y <= x *)
     1.7 -  val less_trans: thm  (* [| x <= y; y <= z |] ==> x <= z *)
     1.8 -  val less_le_trans: thm  (* [| x <= y; y < z |] ==> x < z *)
     1.9 -  val le_less_trans: thm  (* [| x < y; y <= z |] ==> x < z *)
    1.10 -  val le_trans: thm  (* [| x < y; y < z |] ==> x < z *)
    1.11 +  val less_trans: thm  (* [| x < y; y < z |] ==> x < z *)
    1.12 +  val less_le_trans: thm  (* [| x < y; y <= z |] ==> x < z *)
    1.13 +  val le_less_trans: thm  (* [| x <= y; y < z |] ==> x < z *)
    1.14 +  val le_trans: thm  (* [| x <= y; y <= z |] ==> x <= z *)
    1.15    val le_neq_trans : thm (* [| x <= y ; x ~= y |] ==> x < y *)
    1.16    val neq_le_trans : thm (* [| x ~= y ; x <= y |] ==> x < y *)
    1.17  
    1.18 @@ -56,7 +56,8 @@
    1.19    val eq_neq_eq_imp_neq : thm (* [| x = u ; u ~= v ; v = z|] ==> x ~= z *)
    1.20  
    1.21    (* Analysis of premises and conclusion *)
    1.22 -  (* decomp_x (`x Rel y') should yield (x, Rel, y)
    1.23 +  (* decomp_part is for partial_tac, decomp_lin is for linear_tac;
    1.24 +     decomp_x (`x Rel y') should yield (x, Rel, y)
    1.25         where Rel is one of "<", "<=", "~<", "~<=", "=" and "~=",
    1.26         other relation symbols cause an error message *)
    1.27    val decomp_part: Sign.sg -> term -> (term * string * term) option
     2.1 --- a/src/Provers/trancl.ML	Mon Aug 02 10:15:37 2004 +0200
     2.2 +++ b/src/Provers/trancl.ML	Mon Aug 02 10:16:40 2004 +0200
     2.3 @@ -1,10 +1,33 @@
     2.4  (*
     2.5 -  Title:	Transitivity reasoner for partial and linear orders
     2.6 +  Title:	Transitivity reasoner for transitive closures of relations
     2.7    Id:		$Id$
     2.8    Author:	Oliver Kutter
     2.9    Copyright:	TU Muenchen
    2.10  *)
    2.11  
    2.12 +(*
    2.13 +
    2.14 +The packages provides tactics trancl_tac and rtrancl_tac that prove
    2.15 +goals of the form
    2.16 +
    2.17 +   (x,y) : r^+     and     (x,y) : r^* (rtrancl_tac only)
    2.18 +
    2.19 +from premises of the form
    2.20 +
    2.21 +   (x,y) : r,     (x,y) : r^+     and     (x,y) : r^* (rtrancl_tac only)
    2.22 +
    2.23 +by reflexivity and transitivity.  The relation r is determined by inspecting
    2.24 +the conclusion.
    2.25 +
    2.26 +The package is implemented as an ML functor and thus not limited to
    2.27 +particular constructs for transitive and reflexive-transitive
    2.28 +closures, neither need relations be represented as sets of pairs.  In
    2.29 +order to instantiate the package for transitive closure only, supply
    2.30 +dummy theorems to the additional rules for reflexive-transitive
    2.31 +closures, and don't use rtrancl_tac!
    2.32 +
    2.33 +*)
    2.34 +
    2.35  signature TRANCL_ARITH = 
    2.36  sig
    2.37  
    2.38 @@ -30,6 +53,20 @@
    2.39    val rtrancl_trans : thm
    2.40        (* [| (a,b) : r^* ; (b,c) : r^* |] ==> (a,c) : r^* *)
    2.41  
    2.42 +  (* decomp: decompose a premise or conclusion
    2.43 +
    2.44 +     Returns one of the following:
    2.45 +
    2.46 +     None if not an instance of a relation,
    2.47 +     Some (x, y, r, s) if instance of a relation, where
    2.48 +       x: left hand side argument, y: right hand side argument,
    2.49 +       r: the relation,
    2.50 +       s: the kind of closure, one of
    2.51 +            "r":   the relation itself,
    2.52 +            "r^+": transitive closure of the relation,
    2.53 +            "r^*": reflexive-transitive closure of the relation
    2.54 +  *)  
    2.55 +
    2.56    val decomp: term ->  (term * term * term * string) option 
    2.57  
    2.58  end;
    2.59 @@ -48,7 +85,7 @@
    2.60    = Asm of int 
    2.61    | Thm of proof list * thm; 
    2.62  
    2.63 - exception Cannot;
    2.64 + exception Cannot; (* internal exception: raised if no proof can be found *)
    2.65  
    2.66   fun prove asms = 
    2.67    let fun pr (Asm i) = nth_elem (i, asms)
    2.68 @@ -58,23 +95,30 @@
    2.69    
    2.70  (* Internal datatype for inequalities *)
    2.71  datatype rel 
    2.72 -   = R      of term * term * proof  (* just a unknown relation R *)
    2.73 -   | Trans  of term * term * proof  (* R^+ *)
    2.74 +   = Trans  of term * term * proof  (* R^+ *)
    2.75     | RTrans of term * term * proof; (* R^* *)
    2.76     
    2.77   (* Misc functions for datatype rel *)
    2.78 -fun lower (R (x, _, _)) = x
    2.79 -  | lower (Trans (x, _, _)) = x
    2.80 +fun lower (Trans (x, _, _)) = x
    2.81    | lower (RTrans (x,_,_)) = x;
    2.82  
    2.83 -fun upper (R (_, y, _)) = y
    2.84 -  | upper (Trans (_, y, _)) = y
    2.85 +fun upper (Trans (_, y, _)) = y
    2.86    | upper (RTrans (_,y,_)) = y;
    2.87  
    2.88 -fun getprf   (R (_, _, p)) = p
    2.89 -|   getprf   (Trans   (_, _, p)) = p
    2.90 +fun getprf   (Trans   (_, _, p)) = p
    2.91  |   getprf   (RTrans (_,_, p)) = p; 
    2.92   
    2.93 +(* ************************************************************************ *)
    2.94 +(*                                                                          *)
    2.95 +(*  mkasm_trancl Rel (t,n): term -> (term , int) -> rel list                *)
    2.96 +(*                                                                          *)
    2.97 +(*  Analyse assumption t with index n with respect to relation Rel:         *)
    2.98 +(*  If t is of the form "(x, y) : Rel" (or Rel^+), translate to             *)
    2.99 +(*  an object (singleton list) of internal datatype rel.                    *)
   2.100 +(*  Otherwise return empty list.                                            *)
   2.101 +(*                                                                          *)
   2.102 +(* ************************************************************************ *)
   2.103 +
   2.104  fun mkasm_trancl  Rel  (t, n) =
   2.105    case Cls.decomp t of
   2.106      Some (x, y, rel,r) => if rel aconv Rel then  
   2.107 @@ -87,6 +131,17 @@
   2.108      else [] 
   2.109    | None => [];
   2.110    
   2.111 +(* ************************************************************************ *)
   2.112 +(*                                                                          *)
   2.113 +(*  mkasm_rtrancl Rel (t,n): term -> (term , int) -> rel list               *)
   2.114 +(*                                                                          *)
   2.115 +(*  Analyse assumption t with index n with respect to relation Rel:         *)
   2.116 +(*  If t is of the form "(x, y) : Rel" (or Rel^+ or Rel^* ), translate to   *)
   2.117 +(*  an object (singleton list) of internal datatype rel.                    *)
   2.118 +(*  Otherwise return empty list.                                            *)
   2.119 +(*                                                                          *)
   2.120 +(* ************************************************************************ *)
   2.121 +
   2.122  fun mkasm_rtrancl Rel (t, n) =
   2.123    case Cls.decomp t of
   2.124     Some (x, y, rel, r) => if rel aconv Rel then
   2.125 @@ -98,6 +153,19 @@
   2.126     else [] 
   2.127    | None => [];
   2.128  
   2.129 +(* ************************************************************************ *)
   2.130 +(*                                                                          *)
   2.131 +(*  mkconcl_trancl t: term -> (term, rel, proof)                            *)
   2.132 +(*  mkconcl_rtrancl t: term -> (term, rel, proof)                           *)
   2.133 +(*                                                                          *)
   2.134 +(*  Analyse conclusion t:                                                   *)
   2.135 +(*    - must be of form "(x, y) : r^+ (or r^* for rtrancl)                  *)
   2.136 +(*    - returns r                                                           *)
   2.137 +(*    - conclusion in internal form                                         *)
   2.138 +(*    - proof object                                                        *)
   2.139 +(*                                                                          *)
   2.140 +(* ************************************************************************ *)
   2.141 +
   2.142  fun mkconcl_trancl  t =
   2.143    case Cls.decomp t of
   2.144      Some (x, y, rel, r) => (case r of
   2.145 @@ -113,13 +181,25 @@
   2.146      | _     => raise Cannot)
   2.147    | None => raise Cannot;
   2.148  
   2.149 -(* trans. cls. rules *)
   2.150 +(* ************************************************************************ *)
   2.151 +(*                                                                          *)
   2.152 +(*  makeStep (r1, r2): rel * rel -> rel                                     *)
   2.153 +(*                                                                          *)
   2.154 +(*  Apply transitivity to r1 and r2, obtaining a new element of r^+ or r^*, *)
   2.155 +(*  according the following rules:                                          *)
   2.156 +(*                                                                          *)
   2.157 +(* ( (a, b) : r^+ , (b,c) : r^+ ) --> (a,c) : r^+                           *)
   2.158 +(* ( (a, b) : r^* , (b,c) : r^+ ) --> (a,c) : r^+                           *)
   2.159 +(* ( (a, b) : r^+ , (b,c) : r^* ) --> (a,c) : r^+                           *)
   2.160 +(* ( (a, b) : r^* , (b,c) : r^* ) --> (a,c) : r^*                           *)
   2.161 +(*                                                                          *)
   2.162 +(* ************************************************************************ *)
   2.163 +
   2.164  fun makeStep (Trans (a,_,p), Trans(_,c,q))  = Trans (a,c, Thm ([p,q], Cls.trancl_trans))
   2.165  (* refl. + trans. cls. rules *)
   2.166  |   makeStep (RTrans (a,_,p), Trans(_,c,q))  = Trans (a,c, Thm ([p,q], Cls.rtrancl_trancl_trancl))
   2.167  |   makeStep (Trans (a,_,p), RTrans(_,c,q))  = Trans (a,c, Thm ([p,q], Cls.trancl_rtrancl_trancl))   
   2.168 -|   makeStep (RTrans (a,_,p), RTrans(_,c,q))  = RTrans (a,c, Thm ([p,q], Cls.rtrancl_trans))  
   2.169 -|   makeStep (a,b) = error ("trancl_tac: internal error in makeStep: undefined case");
   2.170 +|   makeStep (RTrans (a,_,p), RTrans(_,c,q))  = RTrans (a,c, Thm ([p,q], Cls.rtrancl_trans));
   2.171  
   2.172  (* ******************************************************************* *)
   2.173  (*                                                                     *)
   2.174 @@ -150,6 +230,7 @@
   2.175  (* ********************************************************************** *)
   2.176  (*                                                                        *)
   2.177  (* mkGraph constructs from a list of objects of type rel  a graph g       *)
   2.178 +(* and a list of all edges with label r+.                                 *)
   2.179  (*                                                                        *)
   2.180  (* ********************************************************************** *)
   2.181  
   2.182 @@ -295,7 +376,7 @@
   2.183  (*                  (bool, rel list)                                        *)
   2.184  (*                                                                          *)
   2.185  (*  Searches a path from vertex x to vertex y in Graph g, returns true and  *)
   2.186 -(*  the list of edges of edges if path is found, otherwise false and nil.   *)
   2.187 +(*  the list of edges if path is found, otherwise false and nil.            *)
   2.188  (*                                                                          *)
   2.189  (* ************************************************************************ *) 
   2.190   
   2.191 @@ -330,9 +411,16 @@
   2.192  
   2.193     end;
   2.194  
   2.195 +(* ************************************************************************ *)
   2.196 +(*                                                                          *)
   2.197 +(* findRtranclProof g tranclEdges subgoal:                                  *)
   2.198 +(* (Term.term * (Term.term * rel list) list) -> rel -> proof list           *)
   2.199 +(*                                                                          *)
   2.200 +(* Searches in graph g a proof for subgoal.                                 *)
   2.201 +(*                                                                          *)
   2.202 +(* ************************************************************************ *)
   2.203  
   2.204  fun findRtranclProof g tranclEdges subgoal = 
   2.205 -   (* simple case first *)
   2.206     case subgoal of (RTrans (x,y,_)) => if x aconv y then [Thm ([], Cls.rtrancl_refl)] else (
   2.207       let val (found, path) = findPath (lower subgoal) (upper subgoal) g
   2.208       in 
   2.209 @@ -424,16 +512,11 @@
   2.210    let val (_, subgoal, _) = mkconcl_trancl concl
   2.211        val (found, path) = findPath (lower subgoal) (upper subgoal) g
   2.212    in
   2.213 -
   2.214 -   
   2.215      if found then  [getprf (transPath (tl path, hd path))]
   2.216      else raise Cannot 
   2.217 -   
   2.218    end
   2.219   end;
   2.220    
   2.221 -
   2.222 - 
   2.223  fun solveRtrancl (asms, concl) = 
   2.224   let val (g,tranclEdges) = mkGraph asms
   2.225       val (_, subgoal, _) = mkconcl_rtrancl concl
   2.226 @@ -475,4 +558,3 @@
   2.227  handle  Cannot  => no_tac);
   2.228  
   2.229  end;
   2.230 -