src/Provers/trancl.ML
changeset 15076 4b3d280ef06a
child 15078 8beb68a7afd9
equal deleted inserted replaced
15075:a6cd1a454751 15076:4b3d280ef06a
       
     1 (*
       
     2   Title:	Transitivity reasoner for partial and linear orders
       
     3   Id:		$Id$
       
     4   Author:	Oliver Kutter
       
     5   Copyright:	TU Muenchen
       
     6 *)
       
     7 
       
     8 signature TRANCL_ARITH = 
       
     9 sig
       
    10 
       
    11   (* theorems for transitive closure *)
       
    12 
       
    13   val r_into_trancl : thm
       
    14       (* (a,b) : r ==> (a,b) : r^+ *)
       
    15   val trancl_trans : thm
       
    16       (* [| (a,b) : r^+ ; (b,c) : r^+ |] ==> (a,c) : r^+ *)
       
    17 
       
    18   (* additional theorems for reflexive-transitive closure *)
       
    19 
       
    20   val rtrancl_refl : thm
       
    21       (* (a,a): r^* *)
       
    22   val r_into_rtrancl : thm
       
    23       (* (a,b) : r ==> (a,b) : r^* *)
       
    24   val trancl_into_rtrancl : thm
       
    25       (* (a,b) : r^+ ==> (a,b) : r^* *)
       
    26   val rtrancl_trancl_trancl : thm
       
    27       (* [| (a,b) : r^* ; (b,c) : r^+ |] ==> (a,c) : r^+ *)
       
    28   val trancl_rtrancl_trancl : thm
       
    29       (* [| (a,b) : r^+ ; (b,c) : r^* |] ==> (a,c) : r^+ *)
       
    30   val rtrancl_trans : thm
       
    31       (* [| (a,b) : r^* ; (b,c) : r^* |] ==> (a,c) : r^* *)
       
    32 
       
    33   val decomp: term ->  (term * term * term * string) option 
       
    34 
       
    35 end;
       
    36 
       
    37 signature TRANCL_TAC = 
       
    38 sig
       
    39   val trancl_tac: int -> tactic;
       
    40   val rtrancl_tac: int -> tactic;
       
    41 end;
       
    42 
       
    43 functor Trancl_Tac_Fun (Cls : TRANCL_ARITH): TRANCL_TAC = 
       
    44 struct
       
    45 
       
    46  
       
    47  datatype proof
       
    48   = Asm of int 
       
    49   | Thm of proof list * thm; 
       
    50 
       
    51  exception Cannot;
       
    52 
       
    53  fun prove asms = 
       
    54   let fun pr (Asm i) = nth_elem (i, asms)
       
    55   |       pr (Thm (prfs, thm)) = (map pr prfs) MRS thm
       
    56   in pr end;
       
    57 
       
    58   
       
    59 (* Internal datatype for inequalities *)
       
    60 datatype rel 
       
    61    = R      of term * term * proof  (* just a unknown relation R *)
       
    62    | Trans  of term * term * proof  (* R^+ *)
       
    63    | RTrans of term * term * proof; (* R^* *)
       
    64    
       
    65  (* Misc functions for datatype rel *)
       
    66 fun lower (R (x, _, _)) = x
       
    67   | lower (Trans (x, _, _)) = x
       
    68   | lower (RTrans (x,_,_)) = x;
       
    69 
       
    70 fun upper (R (_, y, _)) = y
       
    71   | upper (Trans (_, y, _)) = y
       
    72   | upper (RTrans (_,y,_)) = y;
       
    73 
       
    74 fun getprf   (R (_, _, p)) = p
       
    75 |   getprf   (Trans   (_, _, p)) = p
       
    76 |   getprf   (RTrans (_,_, p)) = p; 
       
    77  
       
    78 fun mkasm_trancl  Rel  (t, n) =
       
    79   case Cls.decomp t of
       
    80     Some (x, y, rel,r) => if rel aconv Rel then  
       
    81     
       
    82     (case r of
       
    83       "r"   => [Trans (x,y, Thm([Asm n], Cls.r_into_trancl))]
       
    84     | "r+"  => [Trans (x,y, Asm n)]
       
    85     | "r*"  => []
       
    86     | _     => error ("trancl_tac: unknown relation symbol"))
       
    87     else [] 
       
    88   | None => [];
       
    89   
       
    90 fun mkasm_rtrancl Rel (t, n) =
       
    91   case Cls.decomp t of
       
    92    Some (x, y, rel, r) => if rel aconv Rel then
       
    93     (case r of
       
    94       "r"   => [ Trans (x,y, Thm([Asm n], Cls.r_into_trancl))]
       
    95     | "r+"  => [ Trans (x,y, Asm n)]
       
    96     | "r*"  => [ RTrans(x,y, Asm n)]
       
    97     | _     => error ("rtrancl_tac: unknown relation symbol" ))
       
    98    else [] 
       
    99   | None => [];
       
   100 
       
   101 fun mkconcl_trancl  t =
       
   102   case Cls.decomp t of
       
   103     Some (x, y, rel, r) => (case r of
       
   104       "r+"  => (rel, Trans (x,y, Asm ~1), Asm 0)
       
   105     | _     => raise Cannot)
       
   106   | None => raise Cannot;
       
   107 
       
   108 fun mkconcl_rtrancl  t =
       
   109   case Cls.decomp t of
       
   110     Some (x,  y, rel,r ) => (case r of
       
   111       "r+"  => (rel, Trans (x,y, Asm ~1),  Asm 0)
       
   112     | "r*"  => (rel, RTrans (x,y, Asm ~1), Asm 0)
       
   113     | _     => raise Cannot)
       
   114   | None => raise Cannot;
       
   115 
       
   116 (* trans. cls. rules *)
       
   117 fun makeStep (Trans (a,_,p), Trans(_,c,q))  = Trans (a,c, Thm ([p,q], Cls.trancl_trans))
       
   118 (* refl. + trans. cls. rules *)
       
   119 |   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))   
       
   121 |   makeStep (RTrans (a,_,p), RTrans(_,c,q))  = RTrans (a,c, Thm ([p,q], Cls.rtrancl_trans))  
       
   122 |   makeStep (a,b) = error ("makeStep: internal error: undefined case\n"^(makestring a) ^"\n" ^ (makestring b));
       
   123 
       
   124 (* ******************************************************************* *)
       
   125 (*                                                                     *)
       
   126 (* transPath (Clslist, Cls): (rel  list * rel) -> rel                  *)
       
   127 (*                                                                     *)
       
   128 (* If a path represented by a list of elements of type rel is found,   *)
       
   129 (* this needs to be contracted to a single element of type rel.        *)
       
   130 (* Prior to each transitivity step it is checked whether the step is   *)
       
   131 (* valid.                                                              *)
       
   132 (*                                                                     *)
       
   133 (* ******************************************************************* *)
       
   134 
       
   135 fun transPath ([],acc) = acc
       
   136 |   transPath (x::xs,acc) = transPath (xs, makeStep(acc,x))
       
   137       
       
   138 (* ********************************************************************* *)
       
   139 (* Graph functions                                                       *)
       
   140 (* ********************************************************************* *)
       
   141 
       
   142 (* *********************************************************** *)
       
   143 (* Functions for constructing graphs                           *)
       
   144 (* *********************************************************** *)
       
   145 
       
   146 fun addEdge (v,d,[]) = [(v,d)]
       
   147 |   addEdge (v,d,((u,dl)::el)) = if v aconv u then ((v,d@dl)::el)
       
   148     else (u,dl):: (addEdge(v,d,el));
       
   149     
       
   150 (* ********************************************************************** *)
       
   151 (*                                                                        *)
       
   152 (* mkGraph constructs from a list of objects of type rel  a graph g       *)
       
   153 (*                                                                        *)
       
   154 (* ********************************************************************** *)
       
   155 
       
   156 fun mkGraph [] = ([],[])
       
   157 |   mkGraph ys =  
       
   158  let
       
   159   fun buildGraph ([],g,zs) = (g,zs)
       
   160   |   buildGraph (x::xs, g, zs) = 
       
   161         case x of (Trans (_,_,_)) => 
       
   162 	       buildGraph (xs, addEdge((upper x), [],(addEdge ((lower x),[((upper x),x)],g))), x::zs) 
       
   163 	| _ => buildGraph (xs, addEdge((upper x), [],(addEdge ((lower x),[((upper x),x)],g))), zs)
       
   164 in buildGraph (ys, [], []) end;
       
   165 
       
   166 (* *********************************************************************** *)
       
   167 (*                                                                         *)
       
   168 (* adjacent g u : (''a * 'b list ) list -> ''a -> 'b list                  *)
       
   169 (*                                                                         *)
       
   170 (* List of successors of u in graph g                                      *)
       
   171 (*                                                                         *)
       
   172 (* *********************************************************************** *)
       
   173  
       
   174 fun adjacent eq_comp ((v,adj)::el) u = 
       
   175     if eq_comp (u, v) then adj else adjacent eq_comp el u
       
   176 |   adjacent _  []  _ = []  
       
   177 
       
   178 (* *********************************************************************** *)
       
   179 (*                                                                         *)
       
   180 (* dfs eq_comp g u v:                                                      *)
       
   181 (* ('a * 'a -> bool) -> ('a  *( 'a * rel) list) list ->                    *)
       
   182 (* 'a -> 'a -> (bool * ('a * rel) list)                                    *) 
       
   183 (*                                                                         *)
       
   184 (* Depth first search of v from u.                                         *)
       
   185 (* Returns (true, path(u, v)) if successful, otherwise (false, []).        *)
       
   186 (*                                                                         *)
       
   187 (* *********************************************************************** *)
       
   188 
       
   189 fun dfs eq_comp g u v = 
       
   190  let 
       
   191     val pred = ref nil;
       
   192     val visited = ref nil;
       
   193     
       
   194     fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
       
   195     
       
   196     fun dfs_visit u' = 
       
   197     let val _ = visited := u' :: (!visited)
       
   198     
       
   199     fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end;
       
   200     
       
   201     in if been_visited v then () 
       
   202     else (app (fn (v',l) => if been_visited v' then () else (
       
   203        update (v',l); 
       
   204        dfs_visit v'; ()) )) (adjacent eq_comp g u')
       
   205      end
       
   206   in 
       
   207     dfs_visit u; 
       
   208     if (been_visited v) then (true, (!pred)) else (false , [])   
       
   209   end;
       
   210 
       
   211 (* *********************************************************************** *)
       
   212 (*                                                                         *)
       
   213 (* transpose g:                                                            *)
       
   214 (* (''a * ''a list) list -> (''a * ''a list) list                          *)
       
   215 (*                                                                         *)
       
   216 (* Computes transposed graph g' from g                                     *)
       
   217 (* by reversing all edges u -> v to v -> u                                 *)
       
   218 (*                                                                         *)
       
   219 (* *********************************************************************** *)
       
   220 
       
   221 fun transpose eq_comp g =
       
   222   let
       
   223    (* Compute list of reversed edges for each adjacency list *)
       
   224    fun flip (u,(v,l)::el) = (v,(u,l)) :: flip (u,el)
       
   225      | flip (_,nil) = nil
       
   226    
       
   227    (* Compute adjacency list for node u from the list of edges
       
   228       and return a likewise reduced list of edges.  The list of edges
       
   229       is searches for edges starting from u, and these edges are removed. *)
       
   230    fun gather (u,(v,w)::el) =
       
   231     let
       
   232      val (adj,edges) = gather (u,el)
       
   233     in
       
   234      if eq_comp (u, v) then (w::adj,edges)
       
   235      else (adj,(v,w)::edges)
       
   236     end
       
   237    | gather (_,nil) = (nil,nil)
       
   238 
       
   239    (* For every node in the input graph, call gather to find all reachable
       
   240       nodes in the list of edges *)
       
   241    fun assemble ((u,_)::el) edges =
       
   242        let val (adj,edges) = gather (u,edges)
       
   243        in (u,adj) :: assemble el edges
       
   244        end
       
   245      | assemble nil _ = nil
       
   246 
       
   247    (* Compute, for each adjacency list, the list with reversed edges,
       
   248       and concatenate these lists. *)
       
   249    val flipped = foldr (op @) ((map flip g),nil)
       
   250  
       
   251  in assemble g flipped end    
       
   252  
       
   253 (* *********************************************************************** *)
       
   254 (*                                                                         *)
       
   255 (* dfs_reachable eq_comp g u:                                              *)
       
   256 (* (int * int list) list -> int -> int list                                *) 
       
   257 (*                                                                         *)
       
   258 (* Computes list of all nodes reachable from u in g.                       *)
       
   259 (*                                                                         *)
       
   260 (* *********************************************************************** *)
       
   261 
       
   262 fun dfs_reachable eq_comp g u = 
       
   263  let
       
   264   (* List of vertices which have been visited. *)
       
   265   val visited  = ref nil;
       
   266   
       
   267   fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
       
   268 
       
   269   fun dfs_visit g u  =
       
   270       let
       
   271    val _ = visited := u :: !visited
       
   272    val descendents =
       
   273        foldr (fn ((v,l),ds) => if been_visited v then ds
       
   274             else v :: dfs_visit g v @ ds)
       
   275         ( ((adjacent eq_comp g u)) ,nil)
       
   276    in  descendents end
       
   277  
       
   278  in u :: dfs_visit g u end;
       
   279 
       
   280 (* *********************************************************************** *)
       
   281 (*                                                                         *)
       
   282 (* dfs_term_reachable g u:                                                  *)
       
   283 (* (term * term list) list -> term -> term list                            *) 
       
   284 (*                                                                         *)
       
   285 (* Computes list of all nodes reachable from u in g.                       *)
       
   286 (*                                                                         *)
       
   287 (* *********************************************************************** *)
       
   288 
       
   289 fun dfs_term_reachable g u = dfs_reachable (op aconv) g u;
       
   290 
       
   291 (* ************************************************************************ *) 
       
   292 (*                                                                          *)
       
   293 (* findPath x y g: Term.term -> Term.term ->                                *)
       
   294 (*                  (Term.term * (Term.term * rel list) list) ->            *) 
       
   295 (*                  (bool, rel list)                                        *)
       
   296 (*                                                                          *)
       
   297 (*  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.   *)
       
   299 (*                                                                          *)
       
   300 (* ************************************************************************ *) 
       
   301  
       
   302 fun findPath x y g = 
       
   303   let 
       
   304    val (found, tmp) =  dfs (op aconv) g x y ;
       
   305    val pred = map snd tmp;
       
   306 	 
       
   307    fun path x y  =
       
   308     let
       
   309 	 (* find predecessor u of node v and the edge u -> v *)
       
   310 		
       
   311       fun lookup v [] = raise Cannot
       
   312       |   lookup v (e::es) = if (upper e) aconv v then e else lookup v es;
       
   313 		
       
   314       (* traverse path backwards and return list of visited edges *)   
       
   315       fun rev_path v = 
       
   316 	let val l = lookup v pred
       
   317 	    val u = lower l;
       
   318 	in
       
   319 	  if u aconv x then [l] else (rev_path u) @ [l] 
       
   320 	end
       
   321        
       
   322     in rev_path y end;
       
   323 		
       
   324    in 
       
   325 
       
   326      
       
   327       if found then ( (found, (path x y) )) else (found,[])
       
   328    
       
   329      
       
   330 
       
   331    end;
       
   332 
       
   333 
       
   334 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 (
       
   337      let val (found, path) = findPath (lower subgoal) (upper subgoal) g
       
   338      in 
       
   339        if found then (
       
   340           let val path' = (transPath (tl path, hd path))
       
   341 	  in 
       
   342 	   
       
   343 	    case path' of (Trans (_,_,p)) => [Thm ([p], Cls.trancl_into_rtrancl )] 
       
   344 	    | _ => [getprf path']
       
   345 	   
       
   346 	  end
       
   347        )
       
   348        else raise Cannot
       
   349      end
       
   350    )
       
   351    
       
   352 | (Trans (x,y,_)) => (
       
   353  
       
   354   let
       
   355    val Vx = dfs_term_reachable g x;
       
   356    val g' = transpose (op aconv) g;
       
   357    val Vy = dfs_term_reachable g' y;
       
   358    
       
   359    fun processTranclEdges [] = raise Cannot
       
   360    |   processTranclEdges (e::es) = 
       
   361           if (upper e) mem Vx andalso (lower e) mem Vx
       
   362 	  andalso (upper e) mem Vy andalso (lower e) mem Vy
       
   363 	  then (
       
   364 	      
       
   365 	   
       
   366 	    if (lower e) aconv x then (
       
   367 	      if (upper e) aconv y then (
       
   368 	          [(getprf e)] 
       
   369 	      )
       
   370 	      else (
       
   371 	          let 
       
   372 		    val (found,path) = findPath (upper e) y g
       
   373 		  in
       
   374 
       
   375 		   if found then ( 
       
   376 		       [getprf (transPath (path, e))]
       
   377 		      ) else processTranclEdges es
       
   378 		  
       
   379 		  end 
       
   380 	      )   
       
   381 	    )
       
   382 	    else if (upper e) aconv y then (
       
   383 	       let val (xufound,xupath) = findPath x (lower e) g
       
   384 	       in 
       
   385 	       
       
   386 	          if xufound then (
       
   387 		  	    
       
   388 		    let val xuRTranclEdge = transPath (tl xupath, hd xupath)
       
   389 			    val xyTranclEdge = makeStep(xuRTranclEdge,e)
       
   390 				
       
   391 				in [getprf xyTranclEdge] end
       
   392 				
       
   393 	         ) else processTranclEdges es
       
   394 	       
       
   395 	       end
       
   396 	    )
       
   397 	    else ( 
       
   398 	   
       
   399 	        let val (xufound,xupath) = findPath x (lower e) g
       
   400 		    val (vyfound,vypath) = findPath (upper e) y g
       
   401 		 in 
       
   402 		    if xufound then (
       
   403 		         if vyfound then ( 
       
   404 			    let val xuRTranclEdge = transPath (tl xupath, hd xupath)
       
   405 			        val vyRTranclEdge = transPath (tl vypath, hd vypath)
       
   406 				val xyTranclEdge = makeStep (makeStep(xuRTranclEdge,e),vyRTranclEdge)
       
   407 				
       
   408 				in [getprf xyTranclEdge] end
       
   409 				
       
   410 			 ) else processTranclEdges es
       
   411 		    ) 
       
   412 		    else processTranclEdges es
       
   413 		 end
       
   414 	    )
       
   415 	  )
       
   416 	  else processTranclEdges es;
       
   417    in processTranclEdges tranclEdges end )
       
   418 | _ => raise Cannot
       
   419 
       
   420    
       
   421 fun solveTrancl (asms, concl) = 
       
   422  let val (g,_) = mkGraph asms
       
   423  in
       
   424   let val (_, subgoal, _) = mkconcl_trancl concl
       
   425       val (found, path) = findPath (lower subgoal) (upper subgoal) g
       
   426   in
       
   427 
       
   428    
       
   429     if found then  [getprf (transPath (tl path, hd path))]
       
   430     else raise Cannot 
       
   431    
       
   432   end
       
   433  end;
       
   434   
       
   435 
       
   436  
       
   437 fun solveRtrancl (asms, concl) = 
       
   438  let val (g,tranclEdges) = mkGraph asms
       
   439      val (_, subgoal, _) = mkconcl_rtrancl concl
       
   440 in
       
   441   findRtranclProof g tranclEdges subgoal
       
   442 end;
       
   443  
       
   444    
       
   445 val trancl_tac =   SUBGOAL (fn (A, n) =>
       
   446  let
       
   447   val Hs = Logic.strip_assums_hyp A;
       
   448   val C = Logic.strip_assums_concl A;
       
   449   val (rel,subgoals, prf) = mkconcl_trancl C;
       
   450   val prems = flat (ListPair.map (mkasm_trancl rel) (Hs, 0 upto (length Hs - 1)))
       
   451   val prfs = solveTrancl (prems, C);
       
   452 
       
   453  in
       
   454   METAHYPS (fn asms =>
       
   455     let val thms = map (prove asms) prfs
       
   456     in rtac (prove thms prf) 1 end) n
       
   457  end
       
   458 handle  Cannot  => no_tac);
       
   459 
       
   460  
       
   461  
       
   462 val rtrancl_tac =   SUBGOAL (fn (A, n) =>
       
   463  let
       
   464   val Hs = Logic.strip_assums_hyp A;
       
   465   val C = Logic.strip_assums_concl A;
       
   466   val (rel,subgoals, prf) = mkconcl_rtrancl C;
       
   467 
       
   468   val prems = flat (ListPair.map (mkasm_rtrancl rel) (Hs, 0 upto (length Hs - 1)))
       
   469   val prfs = solveRtrancl (prems, C);
       
   470  in
       
   471   METAHYPS (fn asms =>
       
   472     let val thms = map (prove asms) prfs
       
   473     in rtac (prove thms prf) 1 end) n
       
   474  end
       
   475 handle  Cannot  => no_tac);
       
   476 
       
   477 end;
       
   478