src/Provers/trancl.ML
changeset 15098 0726e7b15618
parent 15078 8beb68a7afd9
child 15531 08c8dad8e399
equal deleted inserted replaced
15097:b807858b97bd 15098:0726e7b15618
     1 (*
     1 (*
     2   Title:	Transitivity reasoner for partial and linear orders
     2   Title:	Transitivity reasoner for transitive closures of relations
     3   Id:		$Id$
     3   Id:		$Id$
     4   Author:	Oliver Kutter
     4   Author:	Oliver Kutter
     5   Copyright:	TU Muenchen
     5   Copyright:	TU Muenchen
       
     6 *)
       
     7 
       
     8 (*
       
     9 
       
    10 The packages provides tactics trancl_tac and rtrancl_tac that prove
       
    11 goals of the form
       
    12 
       
    13    (x,y) : r^+     and     (x,y) : r^* (rtrancl_tac only)
       
    14 
       
    15 from premises of the form
       
    16 
       
    17    (x,y) : r,     (x,y) : r^+     and     (x,y) : r^* (rtrancl_tac only)
       
    18 
       
    19 by reflexivity and transitivity.  The relation r is determined by inspecting
       
    20 the conclusion.
       
    21 
       
    22 The package is implemented as an ML functor and thus not limited to
       
    23 particular constructs for transitive and reflexive-transitive
       
    24 closures, neither need relations be represented as sets of pairs.  In
       
    25 order to instantiate the package for transitive closure only, supply
       
    26 dummy theorems to the additional rules for reflexive-transitive
       
    27 closures, and don't use rtrancl_tac!
       
    28 
     6 *)
    29 *)
     7 
    30 
     8 signature TRANCL_ARITH = 
    31 signature TRANCL_ARITH = 
     9 sig
    32 sig
    10 
    33 
    28   val trancl_rtrancl_trancl : thm
    51   val trancl_rtrancl_trancl : thm
    29       (* [| (a,b) : r^+ ; (b,c) : r^* |] ==> (a,c) : r^+ *)
    52       (* [| (a,b) : r^+ ; (b,c) : r^* |] ==> (a,c) : r^+ *)
    30   val rtrancl_trans : thm
    53   val rtrancl_trans : thm
    31       (* [| (a,b) : r^* ; (b,c) : r^* |] ==> (a,c) : r^* *)
    54       (* [| (a,b) : r^* ; (b,c) : r^* |] ==> (a,c) : r^* *)
    32 
    55 
       
    56   (* decomp: decompose a premise or conclusion
       
    57 
       
    58      Returns one of the following:
       
    59 
       
    60      None if not an instance of a relation,
       
    61      Some (x, y, r, s) if instance of a relation, where
       
    62        x: left hand side argument, y: right hand side argument,
       
    63        r: the relation,
       
    64        s: the kind of closure, one of
       
    65             "r":   the relation itself,
       
    66             "r^+": transitive closure of the relation,
       
    67             "r^*": reflexive-transitive closure of the relation
       
    68   *)  
       
    69 
    33   val decomp: term ->  (term * term * term * string) option 
    70   val decomp: term ->  (term * term * term * string) option 
    34 
    71 
    35 end;
    72 end;
    36 
    73 
    37 signature TRANCL_TAC = 
    74 signature TRANCL_TAC = 
    46  
    83  
    47  datatype proof
    84  datatype proof
    48   = Asm of int 
    85   = Asm of int 
    49   | Thm of proof list * thm; 
    86   | Thm of proof list * thm; 
    50 
    87 
    51  exception Cannot;
    88  exception Cannot; (* internal exception: raised if no proof can be found *)
    52 
    89 
    53  fun prove asms = 
    90  fun prove asms = 
    54   let fun pr (Asm i) = nth_elem (i, asms)
    91   let fun pr (Asm i) = nth_elem (i, asms)
    55   |       pr (Thm (prfs, thm)) = (map pr prfs) MRS thm
    92   |       pr (Thm (prfs, thm)) = (map pr prfs) MRS thm
    56   in pr end;
    93   in pr end;
    57 
    94 
    58   
    95   
    59 (* Internal datatype for inequalities *)
    96 (* Internal datatype for inequalities *)
    60 datatype rel 
    97 datatype rel 
    61    = R      of term * term * proof  (* just a unknown relation R *)
    98    = Trans  of term * term * proof  (* R^+ *)
    62    | Trans  of term * term * proof  (* R^+ *)
       
    63    | RTrans of term * term * proof; (* R^* *)
    99    | RTrans of term * term * proof; (* R^* *)
    64    
   100    
    65  (* Misc functions for datatype rel *)
   101  (* Misc functions for datatype rel *)
    66 fun lower (R (x, _, _)) = x
   102 fun lower (Trans (x, _, _)) = x
    67   | lower (Trans (x, _, _)) = x
       
    68   | lower (RTrans (x,_,_)) = x;
   103   | lower (RTrans (x,_,_)) = x;
    69 
   104 
    70 fun upper (R (_, y, _)) = y
   105 fun upper (Trans (_, y, _)) = y
    71   | upper (Trans (_, y, _)) = y
       
    72   | upper (RTrans (_,y,_)) = y;
   106   | upper (RTrans (_,y,_)) = y;
    73 
   107 
    74 fun getprf   (R (_, _, p)) = p
   108 fun getprf   (Trans   (_, _, p)) = p
    75 |   getprf   (Trans   (_, _, p)) = p
       
    76 |   getprf   (RTrans (_,_, p)) = p; 
   109 |   getprf   (RTrans (_,_, p)) = p; 
    77  
   110  
       
   111 (* ************************************************************************ *)
       
   112 (*                                                                          *)
       
   113 (*  mkasm_trancl Rel (t,n): term -> (term , int) -> rel list                *)
       
   114 (*                                                                          *)
       
   115 (*  Analyse assumption t with index n with respect to relation Rel:         *)
       
   116 (*  If t is of the form "(x, y) : Rel" (or Rel^+), translate to             *)
       
   117 (*  an object (singleton list) of internal datatype rel.                    *)
       
   118 (*  Otherwise return empty list.                                            *)
       
   119 (*                                                                          *)
       
   120 (* ************************************************************************ *)
       
   121 
    78 fun mkasm_trancl  Rel  (t, n) =
   122 fun mkasm_trancl  Rel  (t, n) =
    79   case Cls.decomp t of
   123   case Cls.decomp t of
    80     Some (x, y, rel,r) => if rel aconv Rel then  
   124     Some (x, y, rel,r) => if rel aconv Rel then  
    81     
   125     
    82     (case r of
   126     (case r of
    85     | "r*"  => []
   129     | "r*"  => []
    86     | _     => error ("trancl_tac: unknown relation symbol"))
   130     | _     => error ("trancl_tac: unknown relation symbol"))
    87     else [] 
   131     else [] 
    88   | None => [];
   132   | None => [];
    89   
   133   
       
   134 (* ************************************************************************ *)
       
   135 (*                                                                          *)
       
   136 (*  mkasm_rtrancl Rel (t,n): term -> (term , int) -> rel list               *)
       
   137 (*                                                                          *)
       
   138 (*  Analyse assumption t with index n with respect to relation Rel:         *)
       
   139 (*  If t is of the form "(x, y) : Rel" (or Rel^+ or Rel^* ), translate to   *)
       
   140 (*  an object (singleton list) of internal datatype rel.                    *)
       
   141 (*  Otherwise return empty list.                                            *)
       
   142 (*                                                                          *)
       
   143 (* ************************************************************************ *)
       
   144 
    90 fun mkasm_rtrancl Rel (t, n) =
   145 fun mkasm_rtrancl Rel (t, n) =
    91   case Cls.decomp t of
   146   case Cls.decomp t of
    92    Some (x, y, rel, r) => if rel aconv Rel then
   147    Some (x, y, rel, r) => if rel aconv Rel then
    93     (case r of
   148     (case r of
    94       "r"   => [ Trans (x,y, Thm([Asm n], Cls.r_into_trancl))]
   149       "r"   => [ Trans (x,y, Thm([Asm n], Cls.r_into_trancl))]
    96     | "r*"  => [ RTrans(x,y, Asm n)]
   151     | "r*"  => [ RTrans(x,y, Asm n)]
    97     | _     => error ("rtrancl_tac: unknown relation symbol" ))
   152     | _     => error ("rtrancl_tac: unknown relation symbol" ))
    98    else [] 
   153    else [] 
    99   | None => [];
   154   | None => [];
   100 
   155 
       
   156 (* ************************************************************************ *)
       
   157 (*                                                                          *)
       
   158 (*  mkconcl_trancl t: term -> (term, rel, proof)                            *)
       
   159 (*  mkconcl_rtrancl t: term -> (term, rel, proof)                           *)
       
   160 (*                                                                          *)
       
   161 (*  Analyse conclusion t:                                                   *)
       
   162 (*    - must be of form "(x, y) : r^+ (or r^* for rtrancl)                  *)
       
   163 (*    - returns r                                                           *)
       
   164 (*    - conclusion in internal form                                         *)
       
   165 (*    - proof object                                                        *)
       
   166 (*                                                                          *)
       
   167 (* ************************************************************************ *)
       
   168 
   101 fun mkconcl_trancl  t =
   169 fun mkconcl_trancl  t =
   102   case Cls.decomp t of
   170   case Cls.decomp t of
   103     Some (x, y, rel, r) => (case r of
   171     Some (x, y, rel, r) => (case r of
   104       "r+"  => (rel, Trans (x,y, Asm ~1), Asm 0)
   172       "r+"  => (rel, Trans (x,y, Asm ~1), Asm 0)
   105     | _     => raise Cannot)
   173     | _     => raise Cannot)
   111       "r+"  => (rel, Trans (x,y, Asm ~1),  Asm 0)
   179       "r+"  => (rel, Trans (x,y, Asm ~1),  Asm 0)
   112     | "r*"  => (rel, RTrans (x,y, Asm ~1), Asm 0)
   180     | "r*"  => (rel, RTrans (x,y, Asm ~1), Asm 0)
   113     | _     => raise Cannot)
   181     | _     => raise Cannot)
   114   | None => raise Cannot;
   182   | None => raise Cannot;
   115 
   183 
   116 (* trans. cls. rules *)
   184 (* ************************************************************************ *)
       
   185 (*                                                                          *)
       
   186 (*  makeStep (r1, r2): rel * rel -> rel                                     *)
       
   187 (*                                                                          *)
       
   188 (*  Apply transitivity to r1 and r2, obtaining a new element of r^+ or r^*, *)
       
   189 (*  according the following rules:                                          *)
       
   190 (*                                                                          *)
       
   191 (* ( (a, b) : r^+ , (b,c) : r^+ ) --> (a,c) : r^+                           *)
       
   192 (* ( (a, b) : r^* , (b,c) : r^+ ) --> (a,c) : r^+                           *)
       
   193 (* ( (a, b) : r^+ , (b,c) : r^* ) --> (a,c) : r^+                           *)
       
   194 (* ( (a, b) : r^* , (b,c) : r^* ) --> (a,c) : r^*                           *)
       
   195 (*                                                                          *)
       
   196 (* ************************************************************************ *)
       
   197 
   117 fun makeStep (Trans (a,_,p), Trans(_,c,q))  = Trans (a,c, Thm ([p,q], Cls.trancl_trans))
   198 fun makeStep (Trans (a,_,p), Trans(_,c,q))  = Trans (a,c, Thm ([p,q], Cls.trancl_trans))
   118 (* refl. + trans. cls. rules *)
   199 (* refl. + trans. cls. rules *)
   119 |   makeStep (RTrans (a,_,p), Trans(_,c,q))  = Trans (a,c, Thm ([p,q], Cls.rtrancl_trancl_trancl))
   200 |   makeStep (RTrans (a,_,p), Trans(_,c,q))  = Trans (a,c, Thm ([p,q], Cls.rtrancl_trancl_trancl))
   120 |   makeStep (Trans (a,_,p), RTrans(_,c,q))  = Trans (a,c, Thm ([p,q], Cls.trancl_rtrancl_trancl))   
   201 |   makeStep (Trans (a,_,p), RTrans(_,c,q))  = Trans (a,c, Thm ([p,q], Cls.trancl_rtrancl_trancl))   
   121 |   makeStep (RTrans (a,_,p), RTrans(_,c,q))  = RTrans (a,c, Thm ([p,q], Cls.rtrancl_trans))  
   202 |   makeStep (RTrans (a,_,p), RTrans(_,c,q))  = RTrans (a,c, Thm ([p,q], Cls.rtrancl_trans));
   122 |   makeStep (a,b) = error ("trancl_tac: internal error in makeStep: undefined case");
       
   123 
   203 
   124 (* ******************************************************************* *)
   204 (* ******************************************************************* *)
   125 (*                                                                     *)
   205 (*                                                                     *)
   126 (* transPath (Clslist, Cls): (rel  list * rel) -> rel                  *)
   206 (* transPath (Clslist, Cls): (rel  list * rel) -> rel                  *)
   127 (*                                                                     *)
   207 (*                                                                     *)
   148     else (u,dl):: (addEdge(v,d,el));
   228     else (u,dl):: (addEdge(v,d,el));
   149     
   229     
   150 (* ********************************************************************** *)
   230 (* ********************************************************************** *)
   151 (*                                                                        *)
   231 (*                                                                        *)
   152 (* mkGraph constructs from a list of objects of type rel  a graph g       *)
   232 (* mkGraph constructs from a list of objects of type rel  a graph g       *)
       
   233 (* and a list of all edges with label r+.                                 *)
   153 (*                                                                        *)
   234 (*                                                                        *)
   154 (* ********************************************************************** *)
   235 (* ********************************************************************** *)
   155 
   236 
   156 fun mkGraph [] = ([],[])
   237 fun mkGraph [] = ([],[])
   157 |   mkGraph ys =  
   238 |   mkGraph ys =  
   293 (* findPath x y g: Term.term -> Term.term ->                                *)
   374 (* findPath x y g: Term.term -> Term.term ->                                *)
   294 (*                  (Term.term * (Term.term * rel list) list) ->            *) 
   375 (*                  (Term.term * (Term.term * rel list) list) ->            *) 
   295 (*                  (bool, rel list)                                        *)
   376 (*                  (bool, rel list)                                        *)
   296 (*                                                                          *)
   377 (*                                                                          *)
   297 (*  Searches a path from vertex x to vertex y in Graph g, returns true and  *)
   378 (*  Searches a path from vertex x to vertex y in Graph g, returns true and  *)
   298 (*  the list of edges of edges if path is found, otherwise false and nil.   *)
   379 (*  the list of edges if path is found, otherwise false and nil.            *)
   299 (*                                                                          *)
   380 (*                                                                          *)
   300 (* ************************************************************************ *) 
   381 (* ************************************************************************ *) 
   301  
   382  
   302 fun findPath x y g = 
   383 fun findPath x y g = 
   303   let 
   384   let 
   328    
   409    
   329      
   410      
   330 
   411 
   331    end;
   412    end;
   332 
   413 
       
   414 (* ************************************************************************ *)
       
   415 (*                                                                          *)
       
   416 (* findRtranclProof g tranclEdges subgoal:                                  *)
       
   417 (* (Term.term * (Term.term * rel list) list) -> rel -> proof list           *)
       
   418 (*                                                                          *)
       
   419 (* Searches in graph g a proof for subgoal.                                 *)
       
   420 (*                                                                          *)
       
   421 (* ************************************************************************ *)
   333 
   422 
   334 fun findRtranclProof g tranclEdges subgoal = 
   423 fun findRtranclProof g tranclEdges subgoal = 
   335    (* simple case first *)
       
   336    case subgoal of (RTrans (x,y,_)) => if x aconv y then [Thm ([], Cls.rtrancl_refl)] else (
   424    case subgoal of (RTrans (x,y,_)) => if x aconv y then [Thm ([], Cls.rtrancl_refl)] else (
   337      let val (found, path) = findPath (lower subgoal) (upper subgoal) g
   425      let val (found, path) = findPath (lower subgoal) (upper subgoal) g
   338      in 
   426      in 
   339        if found then (
   427        if found then (
   340           let val path' = (transPath (tl path, hd path))
   428           let val path' = (transPath (tl path, hd path))
   422  let val (g,_) = mkGraph asms
   510  let val (g,_) = mkGraph asms
   423  in
   511  in
   424   let val (_, subgoal, _) = mkconcl_trancl concl
   512   let val (_, subgoal, _) = mkconcl_trancl concl
   425       val (found, path) = findPath (lower subgoal) (upper subgoal) g
   513       val (found, path) = findPath (lower subgoal) (upper subgoal) g
   426   in
   514   in
   427 
       
   428    
       
   429     if found then  [getprf (transPath (tl path, hd path))]
   515     if found then  [getprf (transPath (tl path, hd path))]
   430     else raise Cannot 
   516     else raise Cannot 
   431    
       
   432   end
   517   end
   433  end;
   518  end;
   434   
   519   
   435 
       
   436  
       
   437 fun solveRtrancl (asms, concl) = 
   520 fun solveRtrancl (asms, concl) = 
   438  let val (g,tranclEdges) = mkGraph asms
   521  let val (g,tranclEdges) = mkGraph asms
   439      val (_, subgoal, _) = mkconcl_rtrancl concl
   522      val (_, subgoal, _) = mkconcl_rtrancl concl
   440 in
   523 in
   441   findRtranclProof g tranclEdges subgoal
   524   findRtranclProof g tranclEdges subgoal
   473     in rtac (prove thms prf) 1 end) n
   556     in rtac (prove thms prf) 1 end) n
   474  end
   557  end
   475 handle  Cannot  => no_tac);
   558 handle  Cannot  => no_tac);
   476 
   559 
   477 end;
   560 end;
   478