2 Title: Transitivity reasoner for transitive closures of relations
10 The packages provides tactics trancl_tac and rtrancl_tac that prove
13 (x,y) : r^+ and (x,y) : r^* (rtrancl_tac only)
15 from premises of the form
17 (x,y) : r, (x,y) : r^+ and (x,y) : r^* (rtrancl_tac only)
19 by reflexivity and transitivity. The relation r is determined by inspecting
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!
31 signature TRANCL_ARITH =
34 (* theorems for transitive closure *)
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^+ *)
41 (* additional theorems for reflexive-transitive closure *)
43 val rtrancl_refl : thm
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^* *)
56 (* decomp: decompose a premise or conclusion
58 Returns one of the following:
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,
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
70 val decomp: term -> (term * term * term * string) option
74 signature TRANCL_TAC =
76 val trancl_tac: int -> tactic;
77 val rtrancl_tac: int -> tactic;
80 functor Trancl_Tac_Fun (Cls : TRANCL_ARITH): TRANCL_TAC =
86 | Thm of proof list * thm;
88 exception Cannot; (* internal exception: raised if no proof can be found *)
90 fun prove thy r asms =
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
100 (* Internal datatype for inequalities *)
102 = Trans of term * term * proof (* R^+ *)
103 | RTrans of term * term * proof; (* R^* *)
105 (* Misc functions for datatype rel *)
106 fun lower (Trans (x, _, _)) = x
107 | lower (RTrans (x,_,_)) = x;
109 fun upper (Trans (_, y, _)) = y
110 | upper (RTrans (_,y,_)) = y;
112 fun getprf (Trans (_, _, p)) = p
113 | getprf (RTrans (_,_, p)) = p;
115 (* ************************************************************************ *)
117 (* mkasm_trancl Rel (t,n): term -> (term , int) -> rel list *)
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. *)
124 (* ************************************************************************ *)
126 fun mkasm_trancl Rel (t, n) =
128 SOME (x, y, rel,r) => if rel aconv Rel then
131 "r" => [Trans (x,y, Thm([Asm n], Cls.r_into_trancl))]
132 | "r+" => [Trans (x,y, Asm n)]
134 | _ => error ("trancl_tac: unknown relation symbol"))
138 (* ************************************************************************ *)
140 (* mkasm_rtrancl Rel (t,n): term -> (term , int) -> rel list *)
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. *)
147 (* ************************************************************************ *)
149 fun mkasm_rtrancl Rel (t, n) =
151 SOME (x, y, rel, r) => if rel aconv Rel then
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" ))
160 (* ************************************************************************ *)
162 (* mkconcl_trancl t: term -> (term, rel, proof) *)
163 (* mkconcl_rtrancl t: term -> (term, rel, proof) *)
165 (* Analyse conclusion t: *)
166 (* - must be of form "(x, y) : r^+ (or r^* for rtrancl) *)
168 (* - conclusion in internal form *)
171 (* ************************************************************************ *)
173 fun mkconcl_trancl t =
175 SOME (x, y, rel, r) => (case r of
176 "r+" => (rel, Trans (x,y, Asm ~1), Asm 0)
178 | NONE => raise Cannot;
180 fun mkconcl_rtrancl t =
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)
186 | NONE => raise Cannot;
188 (* ************************************************************************ *)
190 (* makeStep (r1, r2): rel * rel -> rel *)
192 (* Apply transitivity to r1 and r2, obtaining a new element of r^+ or r^*, *)
193 (* according the following rules: *)
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^* *)
200 (* ************************************************************************ *)
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));
208 (* ******************************************************************* *)
210 (* transPath (Clslist, Cls): (rel list * rel) -> rel *)
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 *)
217 (* ******************************************************************* *)
219 fun transPath ([],acc) = acc
220 | transPath (x::xs,acc) = transPath (xs, makeStep(acc,x))
222 (* ********************************************************************* *)
223 (* Graph functions *)
224 (* ********************************************************************* *)
226 (* *********************************************************** *)
227 (* Functions for constructing graphs *)
228 (* *********************************************************** *)
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));
234 (* ********************************************************************** *)
236 (* mkGraph constructs from a list of objects of type rel a graph g *)
237 (* and a list of all edges with label r+. *)
239 (* ********************************************************************** *)
241 fun mkGraph [] = ([],[])
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;
251 (* *********************************************************************** *)
253 (* adjacent g u : (''a * 'b list ) list -> ''a -> 'b list *)
255 (* List of successors of u in graph g *)
257 (* *********************************************************************** *)
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 _ [] _ = []
263 (* *********************************************************************** *)
265 (* dfs eq_comp g u v: *)
266 (* ('a * 'a -> bool) -> ('a *( 'a * rel) list) list -> *)
267 (* 'a -> 'a -> (bool * ('a * rel) list) *)
269 (* Depth first search of v from u. *)
270 (* Returns (true, path(u, v)) if successful, otherwise (false, []). *)
272 (* *********************************************************************** *)
274 fun dfs eq_comp g u v =
277 val visited = ref nil;
279 fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
282 let val _ = visited := u' :: (!visited)
284 fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end;
286 in if been_visited v then ()
287 else (app (fn (v',l) => if been_visited v' then () else (
289 dfs_visit v'; ()) )) (adjacent eq_comp g u')
293 if (been_visited v) then (true, (!pred)) else (false , [])
296 (* *********************************************************************** *)
299 (* (''a * ''a list) list -> (''a * ''a list) list *)
301 (* Computes transposed graph g' from g *)
302 (* by reversing all edges u -> v to v -> u *)
304 (* *********************************************************************** *)
306 fun transpose eq_comp g =
308 (* Compute list of reversed edges for each adjacency list *)
309 fun flip (u,(v,l)::el) = (v,(u,l)) :: flip (u,el)
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) =
317 val (adj,edges) = gather (u,el)
319 if eq_comp (u, v) then (w::adj,edges)
320 else (adj,(v,w)::edges)
322 | gather (_,nil) = (nil,nil)
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
330 | assemble nil _ = nil
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)
336 in assemble g flipped end
338 (* *********************************************************************** *)
340 (* dfs_reachable eq_comp g u: *)
341 (* (int * int list) list -> int -> int list *)
343 (* Computes list of all nodes reachable from u in g. *)
345 (* *********************************************************************** *)
347 fun dfs_reachable eq_comp g u =
349 (* List of vertices which have been visited. *)
350 val visited = ref nil;
352 fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
356 val _ = visited := u :: !visited
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)
363 in u :: dfs_visit g u end;
365 (* *********************************************************************** *)
367 (* dfs_term_reachable g u: *)
368 (* (term * term list) list -> term -> term list *)
370 (* Computes list of all nodes reachable from u in g. *)
372 (* *********************************************************************** *)
374 fun dfs_term_reachable g u = dfs_reachable (op aconv) g u;
376 (* ************************************************************************ *)
378 (* findPath x y g: Term.term -> Term.term -> *)
379 (* (Term.term * (Term.term * rel list) list) -> *)
380 (* (bool, rel list) *)
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. *)
385 (* ************************************************************************ *)
389 val (found, tmp) = dfs (op aconv) g x y ;
390 val pred = map snd tmp;
394 (* find predecessor u of node v and the edge u -> v *)
396 fun lookup v [] = raise Cannot
397 | lookup v (e::es) = if (upper e) aconv v then e else lookup v es;
399 (* traverse path backwards and return list of visited edges *)
401 let val l = lookup v pred
404 if u aconv x then [l] else (rev_path u) @ [l]
412 if found then ( (found, (path x y) )) else (found,[])
418 (* ************************************************************************ *)
420 (* findRtranclProof g tranclEdges subgoal: *)
421 (* (Term.term * (Term.term * rel list) list) -> rel -> proof list *)
423 (* Searches in graph g a proof for subgoal. *)
425 (* ************************************************************************ *)
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
432 let val path' = (transPath (tl path, hd path))
435 case path' of (Trans (_,_,p)) => [Thm ([p], Cls.trancl_into_rtrancl )]
436 | _ => [getprf path']
444 | (Trans (x,y,_)) => (
447 val Vx = dfs_term_reachable g x;
448 val g' = transpose (op aconv) g;
449 val Vy = dfs_term_reachable g' y;
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
458 if (lower e) aconv x then (
459 if (upper e) aconv y then (
464 val (found,path) = findPath (upper e) y g
468 [getprf (transPath (path, e))]
469 ) else processTranclEdges es
474 else if (upper e) aconv y then (
475 let val (xufound,xupath) = findPath x (lower e) g
480 let val xuRTranclEdge = transPath (tl xupath, hd xupath)
481 val xyTranclEdge = makeStep(xuRTranclEdge,e)
483 in [getprf xyTranclEdge] end
485 ) else processTranclEdges es
491 let val (xufound,xupath) = findPath x (lower e) g
492 val (vyfound,vypath) = findPath (upper e) y g
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)
500 in [getprf xyTranclEdge] end
502 ) else processTranclEdges es
504 else processTranclEdges es
508 else processTranclEdges es;
509 in processTranclEdges tranclEdges end )
513 fun solveTrancl (asms, concl) =
514 let val (g,_) = mkGraph asms
516 let val (_, subgoal, _) = mkconcl_trancl concl
517 val (found, path) = findPath (lower subgoal) (upper subgoal) g
519 if found then [getprf (transPath (tl path, hd path))]
524 fun solveRtrancl (asms, concl) =
525 let val (g,tranclEdges) = mkGraph asms
526 val (_, subgoal, _) = mkconcl_rtrancl concl
528 findRtranclProof g tranclEdges subgoal
532 val trancl_tac = SUBGOAL (fn (A, n) => fn st =>
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);
543 let val thms = map (prove thy rel asms) prfs
544 in rtac (prove thy rel thms prf) 1 end) n st
546 handle Cannot => no_tac st);
550 val rtrancl_tac = SUBGOAL (fn (A, n) => fn st =>
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;
557 val prems = List.concat (ListPair.map (mkasm_rtrancl rel) (Hs, 0 upto (length Hs - 1)))
558 val prfs = solveRtrancl (prems, C);
561 let val thms = map (prove thy rel asms) prfs
562 in rtac (prove thy rel thms prf) 1 end) n st
564 handle Cannot => no_tac st);