src/Provers/trancl.ML
author wenzelm
Wed Apr 04 00:11:03 2007 +0200 (2007-04-04)
changeset 22578 b0eb5652f210
parent 22257 159bfab776e2
child 26834 87a5b9ec3863
permissions -rw-r--r--
removed obsolete sign_of/sign_of_thm;
     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 thy r asms = 
    91   let
    92     fun inst thm =
    93       let val SOME (_, _, r', _) = Cls.decomp (concl_of thm)
    94       in Drule.cterm_instantiate [(cterm_of thy r', cterm_of thy r)] thm end;
    95     fun pr (Asm i) = List.nth (asms, i)
    96       | pr (Thm (prfs, thm)) = map pr prfs MRS inst thm
    97   in pr end;
    98 
    99   
   100 (* Internal datatype for inequalities *)
   101 datatype rel 
   102    = Trans  of term * term * proof  (* R^+ *)
   103    | RTrans of term * term * proof; (* R^* *)
   104    
   105  (* Misc functions for datatype rel *)
   106 fun lower (Trans (x, _, _)) = x
   107   | lower (RTrans (x,_,_)) = x;
   108 
   109 fun upper (Trans (_, y, _)) = y
   110   | upper (RTrans (_,y,_)) = y;
   111 
   112 fun getprf   (Trans   (_, _, p)) = p
   113 |   getprf   (RTrans (_,_, p)) = p; 
   114  
   115 (* ************************************************************************ *)
   116 (*                                                                          *)
   117 (*  mkasm_trancl Rel (t,n): term -> (term , int) -> rel list                *)
   118 (*                                                                          *)
   119 (*  Analyse assumption t with index n with respect to relation Rel:         *)
   120 (*  If t is of the form "(x, y) : Rel" (or Rel^+), translate to             *)
   121 (*  an object (singleton list) of internal datatype rel.                    *)
   122 (*  Otherwise return empty list.                                            *)
   123 (*                                                                          *)
   124 (* ************************************************************************ *)
   125 
   126 fun mkasm_trancl  Rel  (t, n) =
   127   case Cls.decomp t of
   128     SOME (x, y, rel,r) => if rel aconv Rel then  
   129     
   130     (case r of
   131       "r"   => [Trans (x,y, Thm([Asm n], Cls.r_into_trancl))]
   132     | "r+"  => [Trans (x,y, Asm n)]
   133     | "r*"  => []
   134     | _     => error ("trancl_tac: unknown relation symbol"))
   135     else [] 
   136   | NONE => [];
   137   
   138 (* ************************************************************************ *)
   139 (*                                                                          *)
   140 (*  mkasm_rtrancl Rel (t,n): term -> (term , int) -> rel list               *)
   141 (*                                                                          *)
   142 (*  Analyse assumption t with index n with respect to relation Rel:         *)
   143 (*  If t is of the form "(x, y) : Rel" (or Rel^+ or Rel^* ), translate to   *)
   144 (*  an object (singleton list) of internal datatype rel.                    *)
   145 (*  Otherwise return empty list.                                            *)
   146 (*                                                                          *)
   147 (* ************************************************************************ *)
   148 
   149 fun mkasm_rtrancl Rel (t, n) =
   150   case Cls.decomp t of
   151    SOME (x, y, rel, r) => if rel aconv Rel then
   152     (case r of
   153       "r"   => [ Trans (x,y, Thm([Asm n], Cls.r_into_trancl))]
   154     | "r+"  => [ Trans (x,y, Asm n)]
   155     | "r*"  => [ RTrans(x,y, Asm n)]
   156     | _     => error ("rtrancl_tac: unknown relation symbol" ))
   157    else [] 
   158   | NONE => [];
   159 
   160 (* ************************************************************************ *)
   161 (*                                                                          *)
   162 (*  mkconcl_trancl t: term -> (term, rel, proof)                            *)
   163 (*  mkconcl_rtrancl t: term -> (term, rel, proof)                           *)
   164 (*                                                                          *)
   165 (*  Analyse conclusion t:                                                   *)
   166 (*    - must be of form "(x, y) : r^+ (or r^* for rtrancl)                  *)
   167 (*    - returns r                                                           *)
   168 (*    - conclusion in internal form                                         *)
   169 (*    - proof object                                                        *)
   170 (*                                                                          *)
   171 (* ************************************************************************ *)
   172 
   173 fun mkconcl_trancl  t =
   174   case Cls.decomp t of
   175     SOME (x, y, rel, r) => (case r of
   176       "r+"  => (rel, Trans (x,y, Asm ~1), Asm 0)
   177     | _     => raise Cannot)
   178   | NONE => raise Cannot;
   179 
   180 fun mkconcl_rtrancl  t =
   181   case Cls.decomp t of
   182     SOME (x,  y, rel,r ) => (case r of
   183       "r+"  => (rel, Trans (x,y, Asm ~1),  Asm 0)
   184     | "r*"  => (rel, RTrans (x,y, Asm ~1), Asm 0)
   185     | _     => raise Cannot)
   186   | NONE => raise Cannot;
   187 
   188 (* ************************************************************************ *)
   189 (*                                                                          *)
   190 (*  makeStep (r1, r2): rel * rel -> rel                                     *)
   191 (*                                                                          *)
   192 (*  Apply transitivity to r1 and r2, obtaining a new element of r^+ or r^*, *)
   193 (*  according the following rules:                                          *)
   194 (*                                                                          *)
   195 (* ( (a, b) : r^+ , (b,c) : r^+ ) --> (a,c) : r^+                           *)
   196 (* ( (a, b) : r^* , (b,c) : r^+ ) --> (a,c) : r^+                           *)
   197 (* ( (a, b) : r^+ , (b,c) : r^* ) --> (a,c) : r^+                           *)
   198 (* ( (a, b) : r^* , (b,c) : r^* ) --> (a,c) : r^*                           *)
   199 (*                                                                          *)
   200 (* ************************************************************************ *)
   201 
   202 fun makeStep (Trans (a,_,p), Trans(_,c,q))  = Trans (a,c, Thm ([p,q], Cls.trancl_trans))
   203 (* refl. + trans. cls. rules *)
   204 |   makeStep (RTrans (a,_,p), Trans(_,c,q))  = Trans (a,c, Thm ([p,q], Cls.rtrancl_trancl_trancl))
   205 |   makeStep (Trans (a,_,p), RTrans(_,c,q))  = Trans (a,c, Thm ([p,q], Cls.trancl_rtrancl_trancl))   
   206 |   makeStep (RTrans (a,_,p), RTrans(_,c,q))  = RTrans (a,c, Thm ([p,q], Cls.rtrancl_trans));
   207 
   208 (* ******************************************************************* *)
   209 (*                                                                     *)
   210 (* transPath (Clslist, Cls): (rel  list * rel) -> rel                  *)
   211 (*                                                                     *)
   212 (* If a path represented by a list of elements of type rel is found,   *)
   213 (* this needs to be contracted to a single element of type rel.        *)
   214 (* Prior to each transitivity step it is checked whether the step is   *)
   215 (* valid.                                                              *)
   216 (*                                                                     *)
   217 (* ******************************************************************* *)
   218 
   219 fun transPath ([],acc) = acc
   220 |   transPath (x::xs,acc) = transPath (xs, makeStep(acc,x))
   221       
   222 (* ********************************************************************* *)
   223 (* Graph functions                                                       *)
   224 (* ********************************************************************* *)
   225 
   226 (* *********************************************************** *)
   227 (* Functions for constructing graphs                           *)
   228 (* *********************************************************** *)
   229 
   230 fun addEdge (v,d,[]) = [(v,d)]
   231 |   addEdge (v,d,((u,dl)::el)) = if v aconv u then ((v,d@dl)::el)
   232     else (u,dl):: (addEdge(v,d,el));
   233     
   234 (* ********************************************************************** *)
   235 (*                                                                        *)
   236 (* mkGraph constructs from a list of objects of type rel  a graph g       *)
   237 (* and a list of all edges with label r+.                                 *)
   238 (*                                                                        *)
   239 (* ********************************************************************** *)
   240 
   241 fun mkGraph [] = ([],[])
   242 |   mkGraph ys =  
   243  let
   244   fun buildGraph ([],g,zs) = (g,zs)
   245   |   buildGraph (x::xs, g, zs) = 
   246         case x of (Trans (_,_,_)) => 
   247 	       buildGraph (xs, addEdge((upper x), [],(addEdge ((lower x),[((upper x),x)],g))), x::zs) 
   248 	| _ => buildGraph (xs, addEdge((upper x), [],(addEdge ((lower x),[((upper x),x)],g))), zs)
   249 in buildGraph (ys, [], []) end;
   250 
   251 (* *********************************************************************** *)
   252 (*                                                                         *)
   253 (* adjacent g u : (''a * 'b list ) list -> ''a -> 'b list                  *)
   254 (*                                                                         *)
   255 (* List of successors of u in graph g                                      *)
   256 (*                                                                         *)
   257 (* *********************************************************************** *)
   258  
   259 fun adjacent eq_comp ((v,adj)::el) u = 
   260     if eq_comp (u, v) then adj else adjacent eq_comp el u
   261 |   adjacent _  []  _ = []  
   262 
   263 (* *********************************************************************** *)
   264 (*                                                                         *)
   265 (* dfs eq_comp g u v:                                                      *)
   266 (* ('a * 'a -> bool) -> ('a  *( 'a * rel) list) list ->                    *)
   267 (* 'a -> 'a -> (bool * ('a * rel) list)                                    *) 
   268 (*                                                                         *)
   269 (* Depth first search of v from u.                                         *)
   270 (* Returns (true, path(u, v)) if successful, otherwise (false, []).        *)
   271 (*                                                                         *)
   272 (* *********************************************************************** *)
   273 
   274 fun dfs eq_comp g u v = 
   275  let 
   276     val pred = ref nil;
   277     val visited = ref nil;
   278     
   279     fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
   280     
   281     fun dfs_visit u' = 
   282     let val _ = visited := u' :: (!visited)
   283     
   284     fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end;
   285     
   286     in if been_visited v then () 
   287     else (app (fn (v',l) => if been_visited v' then () else (
   288        update (v',l); 
   289        dfs_visit v'; ()) )) (adjacent eq_comp g u')
   290      end
   291   in 
   292     dfs_visit u; 
   293     if (been_visited v) then (true, (!pred)) else (false , [])   
   294   end;
   295 
   296 (* *********************************************************************** *)
   297 (*                                                                         *)
   298 (* transpose g:                                                            *)
   299 (* (''a * ''a list) list -> (''a * ''a list) list                          *)
   300 (*                                                                         *)
   301 (* Computes transposed graph g' from g                                     *)
   302 (* by reversing all edges u -> v to v -> u                                 *)
   303 (*                                                                         *)
   304 (* *********************************************************************** *)
   305 
   306 fun transpose eq_comp g =
   307   let
   308    (* Compute list of reversed edges for each adjacency list *)
   309    fun flip (u,(v,l)::el) = (v,(u,l)) :: flip (u,el)
   310      | flip (_,nil) = nil
   311    
   312    (* Compute adjacency list for node u from the list of edges
   313       and return a likewise reduced list of edges.  The list of edges
   314       is searches for edges starting from u, and these edges are removed. *)
   315    fun gather (u,(v,w)::el) =
   316     let
   317      val (adj,edges) = gather (u,el)
   318     in
   319      if eq_comp (u, v) then (w::adj,edges)
   320      else (adj,(v,w)::edges)
   321     end
   322    | gather (_,nil) = (nil,nil)
   323 
   324    (* For every node in the input graph, call gather to find all reachable
   325       nodes in the list of edges *)
   326    fun assemble ((u,_)::el) edges =
   327        let val (adj,edges) = gather (u,edges)
   328        in (u,adj) :: assemble el edges
   329        end
   330      | assemble nil _ = nil
   331 
   332    (* Compute, for each adjacency list, the list with reversed edges,
   333       and concatenate these lists. *)
   334    val flipped = foldr (op @) nil (map flip g)
   335  
   336  in assemble g flipped end    
   337  
   338 (* *********************************************************************** *)
   339 (*                                                                         *)
   340 (* dfs_reachable eq_comp g u:                                              *)
   341 (* (int * int list) list -> int -> int list                                *) 
   342 (*                                                                         *)
   343 (* Computes list of all nodes reachable from u in g.                       *)
   344 (*                                                                         *)
   345 (* *********************************************************************** *)
   346 
   347 fun dfs_reachable eq_comp g u = 
   348  let
   349   (* List of vertices which have been visited. *)
   350   val visited  = ref nil;
   351   
   352   fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
   353 
   354   fun dfs_visit g u  =
   355       let
   356    val _ = visited := u :: !visited
   357    val descendents =
   358        foldr (fn ((v,l),ds) => if been_visited v then ds
   359             else v :: dfs_visit g v @ ds)
   360         nil (adjacent eq_comp g u)
   361    in  descendents end
   362  
   363  in u :: dfs_visit g u end;
   364 
   365 (* *********************************************************************** *)
   366 (*                                                                         *)
   367 (* dfs_term_reachable g u:                                                  *)
   368 (* (term * term list) list -> term -> term list                            *) 
   369 (*                                                                         *)
   370 (* Computes list of all nodes reachable from u in g.                       *)
   371 (*                                                                         *)
   372 (* *********************************************************************** *)
   373 
   374 fun dfs_term_reachable g u = dfs_reachable (op aconv) g u;
   375 
   376 (* ************************************************************************ *) 
   377 (*                                                                          *)
   378 (* findPath x y g: Term.term -> Term.term ->                                *)
   379 (*                  (Term.term * (Term.term * rel list) list) ->            *) 
   380 (*                  (bool, rel list)                                        *)
   381 (*                                                                          *)
   382 (*  Searches a path from vertex x to vertex y in Graph g, returns true and  *)
   383 (*  the list of edges if path is found, otherwise false and nil.            *)
   384 (*                                                                          *)
   385 (* ************************************************************************ *) 
   386  
   387 fun findPath x y g = 
   388   let 
   389    val (found, tmp) =  dfs (op aconv) g x y ;
   390    val pred = map snd tmp;
   391 	 
   392    fun path x y  =
   393     let
   394 	 (* find predecessor u of node v and the edge u -> v *)
   395 		
   396       fun lookup v [] = raise Cannot
   397       |   lookup v (e::es) = if (upper e) aconv v then e else lookup v es;
   398 		
   399       (* traverse path backwards and return list of visited edges *)   
   400       fun rev_path v = 
   401 	let val l = lookup v pred
   402 	    val u = lower l;
   403 	in
   404 	  if u aconv x then [l] else (rev_path u) @ [l] 
   405 	end
   406        
   407     in rev_path y end;
   408 		
   409    in 
   410 
   411      
   412       if found then ( (found, (path x y) )) else (found,[])
   413    
   414      
   415 
   416    end;
   417 
   418 (* ************************************************************************ *)
   419 (*                                                                          *)
   420 (* findRtranclProof g tranclEdges subgoal:                                  *)
   421 (* (Term.term * (Term.term * rel list) list) -> rel -> proof list           *)
   422 (*                                                                          *)
   423 (* Searches in graph g a proof for subgoal.                                 *)
   424 (*                                                                          *)
   425 (* ************************************************************************ *)
   426 
   427 fun findRtranclProof g tranclEdges subgoal = 
   428    case subgoal of (RTrans (x,y,_)) => if x aconv y then [Thm ([], Cls.rtrancl_refl)] else (
   429      let val (found, path) = findPath (lower subgoal) (upper subgoal) g
   430      in 
   431        if found then (
   432           let val path' = (transPath (tl path, hd path))
   433 	  in 
   434 	   
   435 	    case path' of (Trans (_,_,p)) => [Thm ([p], Cls.trancl_into_rtrancl )] 
   436 	    | _ => [getprf path']
   437 	   
   438 	  end
   439        )
   440        else raise Cannot
   441      end
   442    )
   443    
   444 | (Trans (x,y,_)) => (
   445  
   446   let
   447    val Vx = dfs_term_reachable g x;
   448    val g' = transpose (op aconv) g;
   449    val Vy = dfs_term_reachable g' y;
   450    
   451    fun processTranclEdges [] = raise Cannot
   452    |   processTranclEdges (e::es) = 
   453           if (upper e) mem Vx andalso (lower e) mem Vx
   454 	  andalso (upper e) mem Vy andalso (lower e) mem Vy
   455 	  then (
   456 	      
   457 	   
   458 	    if (lower e) aconv x then (
   459 	      if (upper e) aconv y then (
   460 	          [(getprf e)] 
   461 	      )
   462 	      else (
   463 	          let 
   464 		    val (found,path) = findPath (upper e) y g
   465 		  in
   466 
   467 		   if found then ( 
   468 		       [getprf (transPath (path, e))]
   469 		      ) else processTranclEdges es
   470 		  
   471 		  end 
   472 	      )   
   473 	    )
   474 	    else if (upper e) aconv y then (
   475 	       let val (xufound,xupath) = findPath x (lower e) g
   476 	       in 
   477 	       
   478 	          if xufound then (
   479 		  	    
   480 		    let val xuRTranclEdge = transPath (tl xupath, hd xupath)
   481 			    val xyTranclEdge = makeStep(xuRTranclEdge,e)
   482 				
   483 				in [getprf xyTranclEdge] end
   484 				
   485 	         ) else processTranclEdges es
   486 	       
   487 	       end
   488 	    )
   489 	    else ( 
   490 	   
   491 	        let val (xufound,xupath) = findPath x (lower e) g
   492 		    val (vyfound,vypath) = findPath (upper e) y g
   493 		 in 
   494 		    if xufound then (
   495 		         if vyfound then ( 
   496 			    let val xuRTranclEdge = transPath (tl xupath, hd xupath)
   497 			        val vyRTranclEdge = transPath (tl vypath, hd vypath)
   498 				val xyTranclEdge = makeStep (makeStep(xuRTranclEdge,e),vyRTranclEdge)
   499 				
   500 				in [getprf xyTranclEdge] end
   501 				
   502 			 ) else processTranclEdges es
   503 		    ) 
   504 		    else processTranclEdges es
   505 		 end
   506 	    )
   507 	  )
   508 	  else processTranclEdges es;
   509    in processTranclEdges tranclEdges end )
   510 | _ => raise Cannot
   511 
   512    
   513 fun solveTrancl (asms, concl) = 
   514  let val (g,_) = mkGraph asms
   515  in
   516   let val (_, subgoal, _) = mkconcl_trancl concl
   517       val (found, path) = findPath (lower subgoal) (upper subgoal) g
   518   in
   519     if found then  [getprf (transPath (tl path, hd path))]
   520     else raise Cannot 
   521   end
   522  end;
   523   
   524 fun solveRtrancl (asms, concl) = 
   525  let val (g,tranclEdges) = mkGraph asms
   526      val (_, subgoal, _) = mkconcl_rtrancl concl
   527 in
   528   findRtranclProof g tranclEdges subgoal
   529 end;
   530  
   531    
   532 val trancl_tac =   SUBGOAL (fn (A, n) => fn st =>
   533  let
   534   val thy = theory_of_thm st;
   535   val Hs = Logic.strip_assums_hyp A;
   536   val C = Logic.strip_assums_concl A;
   537   val (rel,subgoals, prf) = mkconcl_trancl C;
   538   val prems = List.concat (ListPair.map (mkasm_trancl rel) (Hs, 0 upto (length Hs - 1)))
   539   val prfs = solveTrancl (prems, C);
   540 
   541  in
   542   METAHYPS (fn asms =>
   543     let val thms = map (prove thy rel asms) prfs
   544     in rtac (prove thy rel thms prf) 1 end) n st
   545  end
   546 handle  Cannot  => no_tac st);
   547 
   548  
   549  
   550 val rtrancl_tac =   SUBGOAL (fn (A, n) => fn st =>
   551  let
   552   val thy = theory_of_thm st;
   553   val Hs = Logic.strip_assums_hyp A;
   554   val C = Logic.strip_assums_concl A;
   555   val (rel,subgoals, prf) = mkconcl_rtrancl C;
   556 
   557   val prems = List.concat (ListPair.map (mkasm_rtrancl rel) (Hs, 0 upto (length Hs - 1)))
   558   val prfs = solveRtrancl (prems, C);
   559  in
   560   METAHYPS (fn asms =>
   561     let val thms = map (prove thy rel asms) prfs
   562     in rtac (prove thy rel thms prf) 1 end) n st
   563  end
   564 handle  Cannot  => no_tac st);
   565 
   566 end;