src/Provers/trancl.ML
author wenzelm
Thu Dec 07 00:42:04 2006 +0100 (2006-12-07)
changeset 21687 f689f729afab
parent 15574 b1d1b5bfc464
child 22257 159bfab776e2
permissions -rw-r--r--
reorganized structure Goal vs. Tactic;
     1 (*
     2   Title:	Transitivity reasoner for transitive closures of relations
     3   Id:		$Id$
     4   Author:	Oliver Kutter
     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 
    29 *)
    30 
    31 signature TRANCL_ARITH = 
    32 sig
    33 
    34   (* theorems for transitive closure *)
    35 
    36   val r_into_trancl : thm
    37       (* (a,b) : r ==> (a,b) : r^+ *)
    38   val trancl_trans : thm
    39       (* [| (a,b) : r^+ ; (b,c) : r^+ |] ==> (a,c) : r^+ *)
    40 
    41   (* additional theorems for reflexive-transitive closure *)
    42 
    43   val rtrancl_refl : thm
    44       (* (a,a): r^* *)
    45   val r_into_rtrancl : thm
    46       (* (a,b) : r ==> (a,b) : r^* *)
    47   val trancl_into_rtrancl : thm
    48       (* (a,b) : r^+ ==> (a,b) : r^* *)
    49   val rtrancl_trancl_trancl : thm
    50       (* [| (a,b) : r^* ; (b,c) : r^+ |] ==> (a,c) : r^+ *)
    51   val trancl_rtrancl_trancl : thm
    52       (* [| (a,b) : r^+ ; (b,c) : r^* |] ==> (a,c) : r^+ *)
    53   val rtrancl_trans : thm
    54       (* [| (a,b) : r^* ; (b,c) : r^* |] ==> (a,c) : r^* *)
    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 
    70   val decomp: term ->  (term * term * term * string) option 
    71 
    72 end;
    73 
    74 signature TRANCL_TAC = 
    75 sig
    76   val trancl_tac: int -> tactic;
    77   val rtrancl_tac: int -> tactic;
    78 end;
    79 
    80 functor Trancl_Tac_Fun (Cls : TRANCL_ARITH): TRANCL_TAC = 
    81 struct
    82 
    83  
    84  datatype proof
    85   = Asm of int 
    86   | Thm of proof list * thm; 
    87 
    88  exception Cannot; (* internal exception: raised if no proof can be found *)
    89 
    90  fun prove asms = 
    91   let fun pr (Asm i) = List.nth (asms, i)
    92   |       pr (Thm (prfs, thm)) = (map pr prfs) MRS thm
    93   in pr end;
    94 
    95   
    96 (* Internal datatype for inequalities *)
    97 datatype rel 
    98    = Trans  of term * term * proof  (* R^+ *)
    99    | RTrans of term * term * proof; (* R^* *)
   100    
   101  (* Misc functions for datatype rel *)
   102 fun lower (Trans (x, _, _)) = x
   103   | lower (RTrans (x,_,_)) = x;
   104 
   105 fun upper (Trans (_, y, _)) = y
   106   | upper (RTrans (_,y,_)) = y;
   107 
   108 fun getprf   (Trans   (_, _, p)) = p
   109 |   getprf   (RTrans (_,_, p)) = p; 
   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 
   122 fun mkasm_trancl  Rel  (t, n) =
   123   case Cls.decomp t of
   124     SOME (x, y, rel,r) => if rel aconv Rel then  
   125     
   126     (case r of
   127       "r"   => [Trans (x,y, Thm([Asm n], Cls.r_into_trancl))]
   128     | "r+"  => [Trans (x,y, Asm n)]
   129     | "r*"  => []
   130     | _     => error ("trancl_tac: unknown relation symbol"))
   131     else [] 
   132   | NONE => [];
   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 
   145 fun mkasm_rtrancl Rel (t, n) =
   146   case Cls.decomp t of
   147    SOME (x, y, rel, r) => if rel aconv Rel then
   148     (case r of
   149       "r"   => [ Trans (x,y, Thm([Asm n], Cls.r_into_trancl))]
   150     | "r+"  => [ Trans (x,y, Asm n)]
   151     | "r*"  => [ RTrans(x,y, Asm n)]
   152     | _     => error ("rtrancl_tac: unknown relation symbol" ))
   153    else [] 
   154   | NONE => [];
   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 
   169 fun mkconcl_trancl  t =
   170   case Cls.decomp t of
   171     SOME (x, y, rel, r) => (case r of
   172       "r+"  => (rel, Trans (x,y, Asm ~1), Asm 0)
   173     | _     => raise Cannot)
   174   | NONE => raise Cannot;
   175 
   176 fun mkconcl_rtrancl  t =
   177   case Cls.decomp t of
   178     SOME (x,  y, rel,r ) => (case r of
   179       "r+"  => (rel, Trans (x,y, Asm ~1),  Asm 0)
   180     | "r*"  => (rel, RTrans (x,y, Asm ~1), Asm 0)
   181     | _     => raise Cannot)
   182   | NONE => raise Cannot;
   183 
   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 
   198 fun makeStep (Trans (a,_,p), Trans(_,c,q))  = Trans (a,c, Thm ([p,q], Cls.trancl_trans))
   199 (* refl. + trans. cls. rules *)
   200 |   makeStep (RTrans (a,_,p), Trans(_,c,q))  = Trans (a,c, Thm ([p,q], Cls.rtrancl_trancl_trancl))
   201 |   makeStep (Trans (a,_,p), RTrans(_,c,q))  = Trans (a,c, Thm ([p,q], Cls.trancl_rtrancl_trancl))   
   202 |   makeStep (RTrans (a,_,p), RTrans(_,c,q))  = RTrans (a,c, Thm ([p,q], Cls.rtrancl_trans));
   203 
   204 (* ******************************************************************* *)
   205 (*                                                                     *)
   206 (* transPath (Clslist, Cls): (rel  list * rel) -> rel                  *)
   207 (*                                                                     *)
   208 (* If a path represented by a list of elements of type rel is found,   *)
   209 (* this needs to be contracted to a single element of type rel.        *)
   210 (* Prior to each transitivity step it is checked whether the step is   *)
   211 (* valid.                                                              *)
   212 (*                                                                     *)
   213 (* ******************************************************************* *)
   214 
   215 fun transPath ([],acc) = acc
   216 |   transPath (x::xs,acc) = transPath (xs, makeStep(acc,x))
   217       
   218 (* ********************************************************************* *)
   219 (* Graph functions                                                       *)
   220 (* ********************************************************************* *)
   221 
   222 (* *********************************************************** *)
   223 (* Functions for constructing graphs                           *)
   224 (* *********************************************************** *)
   225 
   226 fun addEdge (v,d,[]) = [(v,d)]
   227 |   addEdge (v,d,((u,dl)::el)) = if v aconv u then ((v,d@dl)::el)
   228     else (u,dl):: (addEdge(v,d,el));
   229     
   230 (* ********************************************************************** *)
   231 (*                                                                        *)
   232 (* mkGraph constructs from a list of objects of type rel  a graph g       *)
   233 (* and a list of all edges with label r+.                                 *)
   234 (*                                                                        *)
   235 (* ********************************************************************** *)
   236 
   237 fun mkGraph [] = ([],[])
   238 |   mkGraph ys =  
   239  let
   240   fun buildGraph ([],g,zs) = (g,zs)
   241   |   buildGraph (x::xs, g, zs) = 
   242         case x of (Trans (_,_,_)) => 
   243 	       buildGraph (xs, addEdge((upper x), [],(addEdge ((lower x),[((upper x),x)],g))), x::zs) 
   244 	| _ => buildGraph (xs, addEdge((upper x), [],(addEdge ((lower x),[((upper x),x)],g))), zs)
   245 in buildGraph (ys, [], []) end;
   246 
   247 (* *********************************************************************** *)
   248 (*                                                                         *)
   249 (* adjacent g u : (''a * 'b list ) list -> ''a -> 'b list                  *)
   250 (*                                                                         *)
   251 (* List of successors of u in graph g                                      *)
   252 (*                                                                         *)
   253 (* *********************************************************************** *)
   254  
   255 fun adjacent eq_comp ((v,adj)::el) u = 
   256     if eq_comp (u, v) then adj else adjacent eq_comp el u
   257 |   adjacent _  []  _ = []  
   258 
   259 (* *********************************************************************** *)
   260 (*                                                                         *)
   261 (* dfs eq_comp g u v:                                                      *)
   262 (* ('a * 'a -> bool) -> ('a  *( 'a * rel) list) list ->                    *)
   263 (* 'a -> 'a -> (bool * ('a * rel) list)                                    *) 
   264 (*                                                                         *)
   265 (* Depth first search of v from u.                                         *)
   266 (* Returns (true, path(u, v)) if successful, otherwise (false, []).        *)
   267 (*                                                                         *)
   268 (* *********************************************************************** *)
   269 
   270 fun dfs eq_comp g u v = 
   271  let 
   272     val pred = ref nil;
   273     val visited = ref nil;
   274     
   275     fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
   276     
   277     fun dfs_visit u' = 
   278     let val _ = visited := u' :: (!visited)
   279     
   280     fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end;
   281     
   282     in if been_visited v then () 
   283     else (app (fn (v',l) => if been_visited v' then () else (
   284        update (v',l); 
   285        dfs_visit v'; ()) )) (adjacent eq_comp g u')
   286      end
   287   in 
   288     dfs_visit u; 
   289     if (been_visited v) then (true, (!pred)) else (false , [])   
   290   end;
   291 
   292 (* *********************************************************************** *)
   293 (*                                                                         *)
   294 (* transpose g:                                                            *)
   295 (* (''a * ''a list) list -> (''a * ''a list) list                          *)
   296 (*                                                                         *)
   297 (* Computes transposed graph g' from g                                     *)
   298 (* by reversing all edges u -> v to v -> u                                 *)
   299 (*                                                                         *)
   300 (* *********************************************************************** *)
   301 
   302 fun transpose eq_comp g =
   303   let
   304    (* Compute list of reversed edges for each adjacency list *)
   305    fun flip (u,(v,l)::el) = (v,(u,l)) :: flip (u,el)
   306      | flip (_,nil) = nil
   307    
   308    (* Compute adjacency list for node u from the list of edges
   309       and return a likewise reduced list of edges.  The list of edges
   310       is searches for edges starting from u, and these edges are removed. *)
   311    fun gather (u,(v,w)::el) =
   312     let
   313      val (adj,edges) = gather (u,el)
   314     in
   315      if eq_comp (u, v) then (w::adj,edges)
   316      else (adj,(v,w)::edges)
   317     end
   318    | gather (_,nil) = (nil,nil)
   319 
   320    (* For every node in the input graph, call gather to find all reachable
   321       nodes in the list of edges *)
   322    fun assemble ((u,_)::el) edges =
   323        let val (adj,edges) = gather (u,edges)
   324        in (u,adj) :: assemble el edges
   325        end
   326      | assemble nil _ = nil
   327 
   328    (* Compute, for each adjacency list, the list with reversed edges,
   329       and concatenate these lists. *)
   330    val flipped = foldr (op @) nil (map flip g)
   331  
   332  in assemble g flipped end    
   333  
   334 (* *********************************************************************** *)
   335 (*                                                                         *)
   336 (* dfs_reachable eq_comp g u:                                              *)
   337 (* (int * int list) list -> int -> int list                                *) 
   338 (*                                                                         *)
   339 (* Computes list of all nodes reachable from u in g.                       *)
   340 (*                                                                         *)
   341 (* *********************************************************************** *)
   342 
   343 fun dfs_reachable eq_comp g u = 
   344  let
   345   (* List of vertices which have been visited. *)
   346   val visited  = ref nil;
   347   
   348   fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
   349 
   350   fun dfs_visit g u  =
   351       let
   352    val _ = visited := u :: !visited
   353    val descendents =
   354        foldr (fn ((v,l),ds) => if been_visited v then ds
   355             else v :: dfs_visit g v @ ds)
   356         nil (adjacent eq_comp g u)
   357    in  descendents end
   358  
   359  in u :: dfs_visit g u end;
   360 
   361 (* *********************************************************************** *)
   362 (*                                                                         *)
   363 (* dfs_term_reachable g u:                                                  *)
   364 (* (term * term list) list -> term -> term list                            *) 
   365 (*                                                                         *)
   366 (* Computes list of all nodes reachable from u in g.                       *)
   367 (*                                                                         *)
   368 (* *********************************************************************** *)
   369 
   370 fun dfs_term_reachable g u = dfs_reachable (op aconv) g u;
   371 
   372 (* ************************************************************************ *) 
   373 (*                                                                          *)
   374 (* findPath x y g: Term.term -> Term.term ->                                *)
   375 (*                  (Term.term * (Term.term * rel list) list) ->            *) 
   376 (*                  (bool, rel list)                                        *)
   377 (*                                                                          *)
   378 (*  Searches a path from vertex x to vertex y in Graph g, returns true and  *)
   379 (*  the list of edges if path is found, otherwise false and nil.            *)
   380 (*                                                                          *)
   381 (* ************************************************************************ *) 
   382  
   383 fun findPath x y g = 
   384   let 
   385    val (found, tmp) =  dfs (op aconv) g x y ;
   386    val pred = map snd tmp;
   387 	 
   388    fun path x y  =
   389     let
   390 	 (* find predecessor u of node v and the edge u -> v *)
   391 		
   392       fun lookup v [] = raise Cannot
   393       |   lookup v (e::es) = if (upper e) aconv v then e else lookup v es;
   394 		
   395       (* traverse path backwards and return list of visited edges *)   
   396       fun rev_path v = 
   397 	let val l = lookup v pred
   398 	    val u = lower l;
   399 	in
   400 	  if u aconv x then [l] else (rev_path u) @ [l] 
   401 	end
   402        
   403     in rev_path y end;
   404 		
   405    in 
   406 
   407      
   408       if found then ( (found, (path x y) )) else (found,[])
   409    
   410      
   411 
   412    end;
   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 (* ************************************************************************ *)
   422 
   423 fun findRtranclProof g tranclEdges subgoal = 
   424    case subgoal of (RTrans (x,y,_)) => if x aconv y then [Thm ([], Cls.rtrancl_refl)] else (
   425      let val (found, path) = findPath (lower subgoal) (upper subgoal) g
   426      in 
   427        if found then (
   428           let val path' = (transPath (tl path, hd path))
   429 	  in 
   430 	   
   431 	    case path' of (Trans (_,_,p)) => [Thm ([p], Cls.trancl_into_rtrancl )] 
   432 	    | _ => [getprf path']
   433 	   
   434 	  end
   435        )
   436        else raise Cannot
   437      end
   438    )
   439    
   440 | (Trans (x,y,_)) => (
   441  
   442   let
   443    val Vx = dfs_term_reachable g x;
   444    val g' = transpose (op aconv) g;
   445    val Vy = dfs_term_reachable g' y;
   446    
   447    fun processTranclEdges [] = raise Cannot
   448    |   processTranclEdges (e::es) = 
   449           if (upper e) mem Vx andalso (lower e) mem Vx
   450 	  andalso (upper e) mem Vy andalso (lower e) mem Vy
   451 	  then (
   452 	      
   453 	   
   454 	    if (lower e) aconv x then (
   455 	      if (upper e) aconv y then (
   456 	          [(getprf e)] 
   457 	      )
   458 	      else (
   459 	          let 
   460 		    val (found,path) = findPath (upper e) y g
   461 		  in
   462 
   463 		   if found then ( 
   464 		       [getprf (transPath (path, e))]
   465 		      ) else processTranclEdges es
   466 		  
   467 		  end 
   468 	      )   
   469 	    )
   470 	    else if (upper e) aconv y then (
   471 	       let val (xufound,xupath) = findPath x (lower e) g
   472 	       in 
   473 	       
   474 	          if xufound then (
   475 		  	    
   476 		    let val xuRTranclEdge = transPath (tl xupath, hd xupath)
   477 			    val xyTranclEdge = makeStep(xuRTranclEdge,e)
   478 				
   479 				in [getprf xyTranclEdge] end
   480 				
   481 	         ) else processTranclEdges es
   482 	       
   483 	       end
   484 	    )
   485 	    else ( 
   486 	   
   487 	        let val (xufound,xupath) = findPath x (lower e) g
   488 		    val (vyfound,vypath) = findPath (upper e) y g
   489 		 in 
   490 		    if xufound then (
   491 		         if vyfound then ( 
   492 			    let val xuRTranclEdge = transPath (tl xupath, hd xupath)
   493 			        val vyRTranclEdge = transPath (tl vypath, hd vypath)
   494 				val xyTranclEdge = makeStep (makeStep(xuRTranclEdge,e),vyRTranclEdge)
   495 				
   496 				in [getprf xyTranclEdge] end
   497 				
   498 			 ) else processTranclEdges es
   499 		    ) 
   500 		    else processTranclEdges es
   501 		 end
   502 	    )
   503 	  )
   504 	  else processTranclEdges es;
   505    in processTranclEdges tranclEdges end )
   506 | _ => raise Cannot
   507 
   508    
   509 fun solveTrancl (asms, concl) = 
   510  let val (g,_) = mkGraph asms
   511  in
   512   let val (_, subgoal, _) = mkconcl_trancl concl
   513       val (found, path) = findPath (lower subgoal) (upper subgoal) g
   514   in
   515     if found then  [getprf (transPath (tl path, hd path))]
   516     else raise Cannot 
   517   end
   518  end;
   519   
   520 fun solveRtrancl (asms, concl) = 
   521  let val (g,tranclEdges) = mkGraph asms
   522      val (_, subgoal, _) = mkconcl_rtrancl concl
   523 in
   524   findRtranclProof g tranclEdges subgoal
   525 end;
   526  
   527    
   528 val trancl_tac =   SUBGOAL (fn (A, n) =>
   529  let
   530   val Hs = Logic.strip_assums_hyp A;
   531   val C = Logic.strip_assums_concl A;
   532   val (rel,subgoals, prf) = mkconcl_trancl C;
   533   val prems = List.concat (ListPair.map (mkasm_trancl rel) (Hs, 0 upto (length Hs - 1)))
   534   val prfs = solveTrancl (prems, C);
   535 
   536  in
   537   METAHYPS (fn asms =>
   538     let val thms = map (prove asms) prfs
   539     in rtac (prove thms prf) 1 end) n
   540  end
   541 handle  Cannot  => no_tac);
   542 
   543  
   544  
   545 val rtrancl_tac =   SUBGOAL (fn (A, n) =>
   546  let
   547   val Hs = Logic.strip_assums_hyp A;
   548   val C = Logic.strip_assums_concl A;
   549   val (rel,subgoals, prf) = mkconcl_rtrancl C;
   550 
   551   val prems = List.concat (ListPair.map (mkasm_rtrancl rel) (Hs, 0 upto (length Hs - 1)))
   552   val prfs = solveRtrancl (prems, C);
   553  in
   554   METAHYPS (fn asms =>
   555     let val thms = map (prove asms) prfs
   556     in rtac (prove thms prf) 1 end) n
   557  end
   558 handle  Cannot  => no_tac);
   559 
   560 end;