1 (* Title: Provers/trancl.ML
2 Author: Oliver Kutter, TU Muenchen
4 Transitivity reasoner for transitive closures of relations
9 The packages provides tactics trancl_tac and rtrancl_tac that prove
12 (x,y) : r^+ and (x,y) : r^* (rtrancl_tac only)
14 from premises of the form
16 (x,y) : r, (x,y) : r^+ and (x,y) : r^* (rtrancl_tac only)
18 by reflexivity and transitivity. The relation r is determined by inspecting
21 The package is implemented as an ML functor and thus not limited to
22 particular constructs for transitive and reflexive-transitive
23 closures, neither need relations be represented as sets of pairs. In
24 order to instantiate the package for transitive closure only, supply
25 dummy theorems to the additional rules for reflexive-transitive
26 closures, and don't use rtrancl_tac!
30 signature TRANCL_ARITH =
33 (* theorems for transitive closure *)
35 val r_into_trancl : thm
36 (* (a,b) : r ==> (a,b) : r^+ *)
37 val trancl_trans : thm
38 (* [| (a,b) : r^+ ; (b,c) : r^+ |] ==> (a,c) : r^+ *)
40 (* additional theorems for reflexive-transitive closure *)
42 val rtrancl_refl : thm
44 val r_into_rtrancl : thm
45 (* (a,b) : r ==> (a,b) : r^* *)
46 val trancl_into_rtrancl : thm
47 (* (a,b) : r^+ ==> (a,b) : r^* *)
48 val rtrancl_trancl_trancl : thm
49 (* [| (a,b) : r^* ; (b,c) : r^+ |] ==> (a,c) : r^+ *)
50 val trancl_rtrancl_trancl : thm
51 (* [| (a,b) : r^+ ; (b,c) : r^* |] ==> (a,c) : r^+ *)
52 val rtrancl_trans : thm
53 (* [| (a,b) : r^* ; (b,c) : r^* |] ==> (a,c) : r^* *)
55 (* decomp: decompose a premise or conclusion
57 Returns one of the following:
59 NONE if not an instance of a relation,
60 SOME (x, y, r, s) if instance of a relation, where
61 x: left hand side argument, y: right hand side argument,
63 s: the kind of closure, one of
64 "r": the relation itself,
65 "r^+": transitive closure of the relation,
66 "r^*": reflexive-transitive closure of the relation
69 val decomp: term -> (term * term * term * string) option
73 signature TRANCL_TAC =
75 val trancl_tac: Proof.context -> int -> tactic
76 val rtrancl_tac: Proof.context -> int -> tactic
79 functor Trancl_Tac(Cls: TRANCL_ARITH): TRANCL_TAC =
85 | Thm of proof list * thm;
87 exception Cannot; (* internal exception: raised if no proof can be found *)
89 fun decomp t = Option.map (fn (x, y, rel, r) =>
90 (Envir.beta_eta_contract x, Envir.beta_eta_contract y,
91 Envir.beta_eta_contract rel, r)) (Cls.decomp t);
93 fun prove thy r asms =
96 let val SOME (_, _, r', _) = decomp (concl_of thm)
97 in Drule.cterm_instantiate [(cterm_of thy r', cterm_of thy r)] thm end;
98 fun pr (Asm i) = nth asms i
99 | pr (Thm (prfs, thm)) = map pr prfs MRS inst thm;
103 (* Internal datatype for inequalities *)
105 = Trans of term * term * proof (* R^+ *)
106 | RTrans of term * term * proof; (* R^* *)
108 (* Misc functions for datatype rel *)
109 fun lower (Trans (x, _, _)) = x
110 | lower (RTrans (x,_,_)) = x;
112 fun upper (Trans (_, y, _)) = y
113 | upper (RTrans (_,y,_)) = y;
115 fun getprf (Trans (_, _, p)) = p
116 | getprf (RTrans (_,_, p)) = p;
118 (* ************************************************************************ *)
120 (* mkasm_trancl Rel (t,n): term -> (term , int) -> rel list *)
122 (* Analyse assumption t with index n with respect to relation Rel: *)
123 (* If t is of the form "(x, y) : Rel" (or Rel^+), translate to *)
124 (* an object (singleton list) of internal datatype rel. *)
125 (* Otherwise return empty list. *)
127 (* ************************************************************************ *)
129 fun mkasm_trancl Rel (t, n) =
131 SOME (x, y, rel,r) => if rel aconv Rel then
134 "r" => [Trans (x,y, Thm([Asm n], Cls.r_into_trancl))]
135 | "r+" => [Trans (x,y, Asm n)]
137 | _ => error ("trancl_tac: unknown relation symbol"))
141 (* ************************************************************************ *)
143 (* mkasm_rtrancl Rel (t,n): term -> (term , int) -> rel list *)
145 (* Analyse assumption t with index n with respect to relation Rel: *)
146 (* If t is of the form "(x, y) : Rel" (or Rel^+ or Rel^* ), translate to *)
147 (* an object (singleton list) of internal datatype rel. *)
148 (* Otherwise return empty list. *)
150 (* ************************************************************************ *)
152 fun mkasm_rtrancl Rel (t, n) =
154 SOME (x, y, rel, r) => if rel aconv Rel then
156 "r" => [ Trans (x,y, Thm([Asm n], Cls.r_into_trancl))]
157 | "r+" => [ Trans (x,y, Asm n)]
158 | "r*" => [ RTrans(x,y, Asm n)]
159 | _ => error ("rtrancl_tac: unknown relation symbol" ))
163 (* ************************************************************************ *)
165 (* mkconcl_trancl t: term -> (term, rel, proof) *)
166 (* mkconcl_rtrancl t: term -> (term, rel, proof) *)
168 (* Analyse conclusion t: *)
169 (* - must be of form "(x, y) : r^+ (or r^* for rtrancl) *)
171 (* - conclusion in internal form *)
174 (* ************************************************************************ *)
176 fun mkconcl_trancl t =
178 SOME (x, y, rel, r) => (case r of
179 "r+" => (rel, Trans (x,y, Asm ~1), Asm 0)
181 | NONE => raise Cannot;
183 fun mkconcl_rtrancl t =
185 SOME (x, y, rel,r ) => (case r of
186 "r+" => (rel, Trans (x,y, Asm ~1), Asm 0)
187 | "r*" => (rel, RTrans (x,y, Asm ~1), Asm 0)
189 | NONE => raise Cannot;
191 (* ************************************************************************ *)
193 (* makeStep (r1, r2): rel * rel -> rel *)
195 (* Apply transitivity to r1 and r2, obtaining a new element of r^+ or r^*, *)
196 (* according the following rules: *)
198 (* ( (a, b) : r^+ , (b,c) : r^+ ) --> (a,c) : r^+ *)
199 (* ( (a, b) : r^* , (b,c) : r^+ ) --> (a,c) : r^+ *)
200 (* ( (a, b) : r^+ , (b,c) : r^* ) --> (a,c) : r^+ *)
201 (* ( (a, b) : r^* , (b,c) : r^* ) --> (a,c) : r^* *)
203 (* ************************************************************************ *)
205 fun makeStep (Trans (a,_,p), Trans(_,c,q)) = Trans (a,c, Thm ([p,q], Cls.trancl_trans))
206 (* refl. + trans. cls. rules *)
207 | makeStep (RTrans (a,_,p), Trans(_,c,q)) = Trans (a,c, Thm ([p,q], Cls.rtrancl_trancl_trancl))
208 | makeStep (Trans (a,_,p), RTrans(_,c,q)) = Trans (a,c, Thm ([p,q], Cls.trancl_rtrancl_trancl))
209 | makeStep (RTrans (a,_,p), RTrans(_,c,q)) = RTrans (a,c, Thm ([p,q], Cls.rtrancl_trans));
211 (* ******************************************************************* *)
213 (* transPath (Clslist, Cls): (rel list * rel) -> rel *)
215 (* If a path represented by a list of elements of type rel is found, *)
216 (* this needs to be contracted to a single element of type rel. *)
217 (* Prior to each transitivity step it is checked whether the step is *)
220 (* ******************************************************************* *)
222 fun transPath ([],acc) = acc
223 | transPath (x::xs,acc) = transPath (xs, makeStep(acc,x))
225 (* ********************************************************************* *)
226 (* Graph functions *)
227 (* ********************************************************************* *)
229 (* *********************************************************** *)
230 (* Functions for constructing graphs *)
231 (* *********************************************************** *)
233 fun addEdge (v,d,[]) = [(v,d)]
234 | addEdge (v,d,((u,dl)::el)) = if v aconv u then ((v,d@dl)::el)
235 else (u,dl):: (addEdge(v,d,el));
237 (* ********************************************************************** *)
239 (* mkGraph constructs from a list of objects of type rel a graph g *)
240 (* and a list of all edges with label r+. *)
242 (* ********************************************************************** *)
244 fun mkGraph [] = ([],[])
247 fun buildGraph ([],g,zs) = (g,zs)
248 | buildGraph (x::xs, g, zs) =
249 case x of (Trans (_,_,_)) =>
250 buildGraph (xs, addEdge((upper x), [],(addEdge ((lower x),[((upper x),x)],g))), x::zs)
251 | _ => buildGraph (xs, addEdge((upper x), [],(addEdge ((lower x),[((upper x),x)],g))), zs)
252 in buildGraph (ys, [], []) end;
254 (* *********************************************************************** *)
256 (* adjacent g u : (''a * 'b list ) list -> ''a -> 'b list *)
258 (* List of successors of u in graph g *)
260 (* *********************************************************************** *)
262 fun adjacent eq_comp ((v,adj)::el) u =
263 if eq_comp (u, v) then adj else adjacent eq_comp el u
264 | adjacent _ [] _ = []
266 (* *********************************************************************** *)
268 (* dfs eq_comp g u v: *)
269 (* ('a * 'a -> bool) -> ('a *( 'a * rel) list) list -> *)
270 (* 'a -> 'a -> (bool * ('a * rel) list) *)
272 (* Depth first search of v from u. *)
273 (* Returns (true, path(u, v)) if successful, otherwise (false, []). *)
275 (* *********************************************************************** *)
277 fun dfs eq_comp g u v =
279 val pred = Unsynchronized.ref [];
280 val visited = Unsynchronized.ref [];
282 fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
285 let val _ = visited := u' :: (!visited)
287 fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end;
289 in if been_visited v then ()
290 else (app (fn (v',l) => if been_visited v' then () else (
292 dfs_visit v'; ()) )) (adjacent eq_comp g u')
296 if (been_visited v) then (true, (!pred)) else (false , [])
299 (* *********************************************************************** *)
302 (* (''a * ''a list) list -> (''a * ''a list) list *)
304 (* Computes transposed graph g' from g *)
305 (* by reversing all edges u -> v to v -> u *)
307 (* *********************************************************************** *)
309 fun transpose eq_comp g =
311 (* Compute list of reversed edges for each adjacency list *)
312 fun flip (u,(v,l)::el) = (v,(u,l)) :: flip (u,el)
315 (* Compute adjacency list for node u from the list of edges
316 and return a likewise reduced list of edges. The list of edges
317 is searches for edges starting from u, and these edges are removed. *)
318 fun gather (u,(v,w)::el) =
320 val (adj,edges) = gather (u,el)
322 if eq_comp (u, v) then (w::adj,edges)
323 else (adj,(v,w)::edges)
325 | gather (_,[]) = ([],[])
327 (* For every node in the input graph, call gather to find all reachable
328 nodes in the list of edges *)
329 fun assemble ((u,_)::el) edges =
330 let val (adj,edges) = gather (u,edges)
331 in (u,adj) :: assemble el edges
335 (* Compute, for each adjacency list, the list with reversed edges,
336 and concatenate these lists. *)
337 val flipped = maps flip g
339 in assemble g flipped end
341 (* *********************************************************************** *)
343 (* dfs_reachable eq_comp g u: *)
344 (* (int * int list) list -> int -> int list *)
346 (* Computes list of all nodes reachable from u in g. *)
348 (* *********************************************************************** *)
350 fun dfs_reachable eq_comp g u =
352 (* List of vertices which have been visited. *)
353 val visited = Unsynchronized.ref [];
355 fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
359 val _ = visited := u :: !visited
361 List.foldr (fn ((v,_),ds) => if been_visited v then ds
362 else v :: dfs_visit g v @ ds)
363 [] (adjacent eq_comp g u)
366 in u :: dfs_visit g u end;
368 (* *********************************************************************** *)
370 (* dfs_term_reachable g u: *)
371 (* (term * term list) list -> term -> term list *)
373 (* Computes list of all nodes reachable from u in g. *)
375 (* *********************************************************************** *)
377 fun dfs_term_reachable g u = dfs_reachable (op aconv) g u;
379 (* ************************************************************************ *)
381 (* findPath x y g: Term.term -> Term.term -> *)
382 (* (Term.term * (Term.term * rel list) list) -> *)
383 (* (bool, rel list) *)
385 (* Searches a path from vertex x to vertex y in Graph g, returns true and *)
386 (* the list of edges if path is found, otherwise false and nil. *)
388 (* ************************************************************************ *)
392 val (found, tmp) = dfs (op aconv) g x y ;
393 val pred = map snd tmp;
397 (* find predecessor u of node v and the edge u -> v *)
399 fun lookup v [] = raise Cannot
400 | lookup v (e::es) = if (upper e) aconv v then e else lookup v es;
402 (* traverse path backwards and return list of visited edges *)
404 let val l = lookup v pred
407 if u aconv x then [l] else (rev_path u) @ [l]
415 if found then ( (found, (path x y) )) else (found,[])
421 (* ************************************************************************ *)
423 (* findRtranclProof g tranclEdges subgoal: *)
424 (* (Term.term * (Term.term * rel list) list) -> rel -> proof list *)
426 (* Searches in graph g a proof for subgoal. *)
428 (* ************************************************************************ *)
430 fun findRtranclProof g tranclEdges subgoal =
431 case subgoal of (RTrans (x,y,_)) => if x aconv y then [Thm ([], Cls.rtrancl_refl)] else (
432 let val (found, path) = findPath (lower subgoal) (upper subgoal) g
435 let val path' = (transPath (tl path, hd path))
438 case path' of (Trans (_,_,p)) => [Thm ([p], Cls.trancl_into_rtrancl )]
439 | _ => [getprf path']
447 | (Trans (x,y,_)) => (
450 val Vx = dfs_term_reachable g x;
451 val g' = transpose (op aconv) g;
452 val Vy = dfs_term_reachable g' y;
454 fun processTranclEdges [] = raise Cannot
455 | processTranclEdges (e::es) =
456 if member (op =) Vx (upper e) andalso member (op =) Vx (lower e)
457 andalso member (op =) Vy (upper e) andalso member (op =) Vy (lower e)
461 if (lower e) aconv x then (
462 if (upper e) aconv y then (
467 val (found,path) = findPath (upper e) y g
471 [getprf (transPath (path, e))]
472 ) else processTranclEdges es
477 else if (upper e) aconv y then (
478 let val (xufound,xupath) = findPath x (lower e) g
483 let val xuRTranclEdge = transPath (tl xupath, hd xupath)
484 val xyTranclEdge = makeStep(xuRTranclEdge,e)
486 in [getprf xyTranclEdge] end
488 ) else processTranclEdges es
494 let val (xufound,xupath) = findPath x (lower e) g
495 val (vyfound,vypath) = findPath (upper e) y g
499 let val xuRTranclEdge = transPath (tl xupath, hd xupath)
500 val vyRTranclEdge = transPath (tl vypath, hd vypath)
501 val xyTranclEdge = makeStep (makeStep(xuRTranclEdge,e),vyRTranclEdge)
503 in [getprf xyTranclEdge] end
505 ) else processTranclEdges es
507 else processTranclEdges es
511 else processTranclEdges es;
512 in processTranclEdges tranclEdges end )
515 fun solveTrancl (asms, concl) =
516 let val (g,_) = mkGraph asms
518 let val (_, subgoal, _) = mkconcl_trancl concl
519 val (found, path) = findPath (lower subgoal) (upper subgoal) g
521 if found then [getprf (transPath (tl path, hd path))]
526 fun solveRtrancl (asms, concl) =
527 let val (g,tranclEdges) = mkGraph asms
528 val (_, subgoal, _) = mkconcl_rtrancl concl
530 findRtranclProof g tranclEdges subgoal
534 fun trancl_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
536 val thy = Proof_Context.theory_of ctxt;
537 val Hs = Logic.strip_assums_hyp A;
538 val C = Logic.strip_assums_concl A;
539 val (rel, _, prf) = mkconcl_trancl C;
541 val prems = flat (map_index (mkasm_trancl rel o swap) Hs);
542 val prfs = solveTrancl (prems, C);
544 Subgoal.FOCUS (fn {prems, concl, ...} =>
546 val SOME (_, _, rel', _) = decomp (term_of concl);
547 val thms = map (prove thy rel' prems) prfs
548 in rtac (prove thy rel' thms prf) 1 end) ctxt n st
550 handle Cannot => Seq.empty);
553 fun rtrancl_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
555 val thy = Proof_Context.theory_of ctxt;
556 val Hs = Logic.strip_assums_hyp A;
557 val C = Logic.strip_assums_concl A;
558 val (rel, _, prf) = mkconcl_rtrancl C;
560 val prems = flat (map_index (mkasm_rtrancl rel o swap) Hs);
561 val prfs = solveRtrancl (prems, C);
563 Subgoal.FOCUS (fn {prems, concl, ...} =>
565 val SOME (_, _, rel', _) = decomp (term_of concl);
566 val thms = map (prove thy rel' prems) prfs
567 in rtac (prove thy rel' thms prf) 1 end) ctxt n st
569 handle Cannot => Seq.empty | General.Subscript => Seq.empty);