ballarin@15076
|
1 |
(*
|
ballarin@15098
|
2 |
Title: Transitivity reasoner for transitive closures of relations
|
ballarin@15076
|
3 |
Id: $Id$
|
ballarin@15076
|
4 |
Author: Oliver Kutter
|
ballarin@15076
|
5 |
Copyright: TU Muenchen
|
ballarin@15076
|
6 |
*)
|
ballarin@15076
|
7 |
|
ballarin@15098
|
8 |
(*
|
ballarin@15098
|
9 |
|
ballarin@15098
|
10 |
The packages provides tactics trancl_tac and rtrancl_tac that prove
|
ballarin@15098
|
11 |
goals of the form
|
ballarin@15098
|
12 |
|
ballarin@15098
|
13 |
(x,y) : r^+ and (x,y) : r^* (rtrancl_tac only)
|
ballarin@15098
|
14 |
|
ballarin@15098
|
15 |
from premises of the form
|
ballarin@15098
|
16 |
|
ballarin@15098
|
17 |
(x,y) : r, (x,y) : r^+ and (x,y) : r^* (rtrancl_tac only)
|
ballarin@15098
|
18 |
|
ballarin@15098
|
19 |
by reflexivity and transitivity. The relation r is determined by inspecting
|
ballarin@15098
|
20 |
the conclusion.
|
ballarin@15098
|
21 |
|
ballarin@15098
|
22 |
The package is implemented as an ML functor and thus not limited to
|
ballarin@15098
|
23 |
particular constructs for transitive and reflexive-transitive
|
ballarin@15098
|
24 |
closures, neither need relations be represented as sets of pairs. In
|
ballarin@15098
|
25 |
order to instantiate the package for transitive closure only, supply
|
ballarin@15098
|
26 |
dummy theorems to the additional rules for reflexive-transitive
|
ballarin@15098
|
27 |
closures, and don't use rtrancl_tac!
|
ballarin@15098
|
28 |
|
ballarin@15098
|
29 |
*)
|
ballarin@15098
|
30 |
|
ballarin@15076
|
31 |
signature TRANCL_ARITH =
|
ballarin@15076
|
32 |
sig
|
ballarin@15076
|
33 |
|
ballarin@15076
|
34 |
(* theorems for transitive closure *)
|
ballarin@15076
|
35 |
|
ballarin@15076
|
36 |
val r_into_trancl : thm
|
ballarin@15076
|
37 |
(* (a,b) : r ==> (a,b) : r^+ *)
|
ballarin@15076
|
38 |
val trancl_trans : thm
|
ballarin@15076
|
39 |
(* [| (a,b) : r^+ ; (b,c) : r^+ |] ==> (a,c) : r^+ *)
|
ballarin@15076
|
40 |
|
ballarin@15076
|
41 |
(* additional theorems for reflexive-transitive closure *)
|
ballarin@15076
|
42 |
|
ballarin@15076
|
43 |
val rtrancl_refl : thm
|
ballarin@15076
|
44 |
(* (a,a): r^* *)
|
ballarin@15076
|
45 |
val r_into_rtrancl : thm
|
ballarin@15076
|
46 |
(* (a,b) : r ==> (a,b) : r^* *)
|
ballarin@15076
|
47 |
val trancl_into_rtrancl : thm
|
ballarin@15076
|
48 |
(* (a,b) : r^+ ==> (a,b) : r^* *)
|
ballarin@15076
|
49 |
val rtrancl_trancl_trancl : thm
|
ballarin@15076
|
50 |
(* [| (a,b) : r^* ; (b,c) : r^+ |] ==> (a,c) : r^+ *)
|
ballarin@15076
|
51 |
val trancl_rtrancl_trancl : thm
|
ballarin@15076
|
52 |
(* [| (a,b) : r^+ ; (b,c) : r^* |] ==> (a,c) : r^+ *)
|
ballarin@15076
|
53 |
val rtrancl_trans : thm
|
ballarin@15076
|
54 |
(* [| (a,b) : r^* ; (b,c) : r^* |] ==> (a,c) : r^* *)
|
ballarin@15076
|
55 |
|
ballarin@15098
|
56 |
(* decomp: decompose a premise or conclusion
|
ballarin@15098
|
57 |
|
ballarin@15098
|
58 |
Returns one of the following:
|
ballarin@15098
|
59 |
|
skalberg@15531
|
60 |
NONE if not an instance of a relation,
|
skalberg@15531
|
61 |
SOME (x, y, r, s) if instance of a relation, where
|
ballarin@15098
|
62 |
x: left hand side argument, y: right hand side argument,
|
ballarin@15098
|
63 |
r: the relation,
|
ballarin@15098
|
64 |
s: the kind of closure, one of
|
ballarin@15098
|
65 |
"r": the relation itself,
|
ballarin@15098
|
66 |
"r^+": transitive closure of the relation,
|
ballarin@15098
|
67 |
"r^*": reflexive-transitive closure of the relation
|
ballarin@15098
|
68 |
*)
|
ballarin@15098
|
69 |
|
ballarin@15076
|
70 |
val decomp: term -> (term * term * term * string) option
|
ballarin@15076
|
71 |
|
ballarin@15076
|
72 |
end;
|
ballarin@15076
|
73 |
|
ballarin@15076
|
74 |
signature TRANCL_TAC =
|
ballarin@15076
|
75 |
sig
|
ballarin@15076
|
76 |
val trancl_tac: int -> tactic;
|
ballarin@15076
|
77 |
val rtrancl_tac: int -> tactic;
|
ballarin@15076
|
78 |
end;
|
ballarin@15076
|
79 |
|
ballarin@15076
|
80 |
functor Trancl_Tac_Fun (Cls : TRANCL_ARITH): TRANCL_TAC =
|
ballarin@15076
|
81 |
struct
|
ballarin@15076
|
82 |
|
ballarin@15076
|
83 |
|
ballarin@15076
|
84 |
datatype proof
|
ballarin@15076
|
85 |
= Asm of int
|
ballarin@15076
|
86 |
| Thm of proof list * thm;
|
ballarin@15076
|
87 |
|
ballarin@15098
|
88 |
exception Cannot; (* internal exception: raised if no proof can be found *)
|
ballarin@15076
|
89 |
|
ballarin@15076
|
90 |
fun prove asms =
|
skalberg@15570
|
91 |
let fun pr (Asm i) = List.nth (asms, i)
|
ballarin@15076
|
92 |
| pr (Thm (prfs, thm)) = (map pr prfs) MRS thm
|
ballarin@15076
|
93 |
in pr end;
|
ballarin@15076
|
94 |
|
ballarin@15076
|
95 |
|
ballarin@15076
|
96 |
(* Internal datatype for inequalities *)
|
ballarin@15076
|
97 |
datatype rel
|
ballarin@15098
|
98 |
= Trans of term * term * proof (* R^+ *)
|
ballarin@15076
|
99 |
| RTrans of term * term * proof; (* R^* *)
|
ballarin@15076
|
100 |
|
ballarin@15076
|
101 |
(* Misc functions for datatype rel *)
|
ballarin@15098
|
102 |
fun lower (Trans (x, _, _)) = x
|
ballarin@15076
|
103 |
| lower (RTrans (x,_,_)) = x;
|
ballarin@15076
|
104 |
|
ballarin@15098
|
105 |
fun upper (Trans (_, y, _)) = y
|
ballarin@15076
|
106 |
| upper (RTrans (_,y,_)) = y;
|
ballarin@15076
|
107 |
|
ballarin@15098
|
108 |
fun getprf (Trans (_, _, p)) = p
|
ballarin@15076
|
109 |
| getprf (RTrans (_,_, p)) = p;
|
ballarin@15076
|
110 |
|
ballarin@15098
|
111 |
(* ************************************************************************ *)
|
ballarin@15098
|
112 |
(* *)
|
ballarin@15098
|
113 |
(* mkasm_trancl Rel (t,n): term -> (term , int) -> rel list *)
|
ballarin@15098
|
114 |
(* *)
|
ballarin@15098
|
115 |
(* Analyse assumption t with index n with respect to relation Rel: *)
|
ballarin@15098
|
116 |
(* If t is of the form "(x, y) : Rel" (or Rel^+), translate to *)
|
ballarin@15098
|
117 |
(* an object (singleton list) of internal datatype rel. *)
|
ballarin@15098
|
118 |
(* Otherwise return empty list. *)
|
ballarin@15098
|
119 |
(* *)
|
ballarin@15098
|
120 |
(* ************************************************************************ *)
|
ballarin@15098
|
121 |
|
ballarin@15076
|
122 |
fun mkasm_trancl Rel (t, n) =
|
ballarin@15076
|
123 |
case Cls.decomp t of
|
skalberg@15531
|
124 |
SOME (x, y, rel,r) => if rel aconv Rel then
|
ballarin@15076
|
125 |
|
ballarin@15076
|
126 |
(case r of
|
ballarin@15076
|
127 |
"r" => [Trans (x,y, Thm([Asm n], Cls.r_into_trancl))]
|
ballarin@15076
|
128 |
| "r+" => [Trans (x,y, Asm n)]
|
ballarin@15076
|
129 |
| "r*" => []
|
ballarin@15076
|
130 |
| _ => error ("trancl_tac: unknown relation symbol"))
|
ballarin@15076
|
131 |
else []
|
skalberg@15531
|
132 |
| NONE => [];
|
ballarin@15076
|
133 |
|
ballarin@15098
|
134 |
(* ************************************************************************ *)
|
ballarin@15098
|
135 |
(* *)
|
ballarin@15098
|
136 |
(* mkasm_rtrancl Rel (t,n): term -> (term , int) -> rel list *)
|
ballarin@15098
|
137 |
(* *)
|
ballarin@15098
|
138 |
(* Analyse assumption t with index n with respect to relation Rel: *)
|
ballarin@15098
|
139 |
(* If t is of the form "(x, y) : Rel" (or Rel^+ or Rel^* ), translate to *)
|
ballarin@15098
|
140 |
(* an object (singleton list) of internal datatype rel. *)
|
ballarin@15098
|
141 |
(* Otherwise return empty list. *)
|
ballarin@15098
|
142 |
(* *)
|
ballarin@15098
|
143 |
(* ************************************************************************ *)
|
ballarin@15098
|
144 |
|
ballarin@15076
|
145 |
fun mkasm_rtrancl Rel (t, n) =
|
ballarin@15076
|
146 |
case Cls.decomp t of
|
skalberg@15531
|
147 |
SOME (x, y, rel, r) => if rel aconv Rel then
|
ballarin@15076
|
148 |
(case r of
|
ballarin@15076
|
149 |
"r" => [ Trans (x,y, Thm([Asm n], Cls.r_into_trancl))]
|
ballarin@15076
|
150 |
| "r+" => [ Trans (x,y, Asm n)]
|
ballarin@15076
|
151 |
| "r*" => [ RTrans(x,y, Asm n)]
|
ballarin@15076
|
152 |
| _ => error ("rtrancl_tac: unknown relation symbol" ))
|
ballarin@15076
|
153 |
else []
|
skalberg@15531
|
154 |
| NONE => [];
|
ballarin@15076
|
155 |
|
ballarin@15098
|
156 |
(* ************************************************************************ *)
|
ballarin@15098
|
157 |
(* *)
|
ballarin@15098
|
158 |
(* mkconcl_trancl t: term -> (term, rel, proof) *)
|
ballarin@15098
|
159 |
(* mkconcl_rtrancl t: term -> (term, rel, proof) *)
|
ballarin@15098
|
160 |
(* *)
|
ballarin@15098
|
161 |
(* Analyse conclusion t: *)
|
ballarin@15098
|
162 |
(* - must be of form "(x, y) : r^+ (or r^* for rtrancl) *)
|
ballarin@15098
|
163 |
(* - returns r *)
|
ballarin@15098
|
164 |
(* - conclusion in internal form *)
|
ballarin@15098
|
165 |
(* - proof object *)
|
ballarin@15098
|
166 |
(* *)
|
ballarin@15098
|
167 |
(* ************************************************************************ *)
|
ballarin@15098
|
168 |
|
ballarin@15076
|
169 |
fun mkconcl_trancl t =
|
ballarin@15076
|
170 |
case Cls.decomp t of
|
skalberg@15531
|
171 |
SOME (x, y, rel, r) => (case r of
|
ballarin@15076
|
172 |
"r+" => (rel, Trans (x,y, Asm ~1), Asm 0)
|
ballarin@15076
|
173 |
| _ => raise Cannot)
|
skalberg@15531
|
174 |
| NONE => raise Cannot;
|
ballarin@15076
|
175 |
|
ballarin@15076
|
176 |
fun mkconcl_rtrancl t =
|
ballarin@15076
|
177 |
case Cls.decomp t of
|
skalberg@15531
|
178 |
SOME (x, y, rel,r ) => (case r of
|
ballarin@15076
|
179 |
"r+" => (rel, Trans (x,y, Asm ~1), Asm 0)
|
ballarin@15076
|
180 |
| "r*" => (rel, RTrans (x,y, Asm ~1), Asm 0)
|
ballarin@15076
|
181 |
| _ => raise Cannot)
|
skalberg@15531
|
182 |
| NONE => raise Cannot;
|
ballarin@15076
|
183 |
|
ballarin@15098
|
184 |
(* ************************************************************************ *)
|
ballarin@15098
|
185 |
(* *)
|
ballarin@15098
|
186 |
(* makeStep (r1, r2): rel * rel -> rel *)
|
ballarin@15098
|
187 |
(* *)
|
ballarin@15098
|
188 |
(* Apply transitivity to r1 and r2, obtaining a new element of r^+ or r^*, *)
|
ballarin@15098
|
189 |
(* according the following rules: *)
|
ballarin@15098
|
190 |
(* *)
|
ballarin@15098
|
191 |
(* ( (a, b) : r^+ , (b,c) : r^+ ) --> (a,c) : r^+ *)
|
ballarin@15098
|
192 |
(* ( (a, b) : r^* , (b,c) : r^+ ) --> (a,c) : r^+ *)
|
ballarin@15098
|
193 |
(* ( (a, b) : r^+ , (b,c) : r^* ) --> (a,c) : r^+ *)
|
ballarin@15098
|
194 |
(* ( (a, b) : r^* , (b,c) : r^* ) --> (a,c) : r^* *)
|
ballarin@15098
|
195 |
(* *)
|
ballarin@15098
|
196 |
(* ************************************************************************ *)
|
ballarin@15098
|
197 |
|
ballarin@15076
|
198 |
fun makeStep (Trans (a,_,p), Trans(_,c,q)) = Trans (a,c, Thm ([p,q], Cls.trancl_trans))
|
ballarin@15076
|
199 |
(* refl. + trans. cls. rules *)
|
ballarin@15076
|
200 |
| makeStep (RTrans (a,_,p), Trans(_,c,q)) = Trans (a,c, Thm ([p,q], Cls.rtrancl_trancl_trancl))
|
ballarin@15076
|
201 |
| makeStep (Trans (a,_,p), RTrans(_,c,q)) = Trans (a,c, Thm ([p,q], Cls.trancl_rtrancl_trancl))
|
ballarin@15098
|
202 |
| makeStep (RTrans (a,_,p), RTrans(_,c,q)) = RTrans (a,c, Thm ([p,q], Cls.rtrancl_trans));
|
ballarin@15076
|
203 |
|
ballarin@15076
|
204 |
(* ******************************************************************* *)
|
ballarin@15076
|
205 |
(* *)
|
ballarin@15076
|
206 |
(* transPath (Clslist, Cls): (rel list * rel) -> rel *)
|
ballarin@15076
|
207 |
(* *)
|
ballarin@15076
|
208 |
(* If a path represented by a list of elements of type rel is found, *)
|
ballarin@15076
|
209 |
(* this needs to be contracted to a single element of type rel. *)
|
ballarin@15076
|
210 |
(* Prior to each transitivity step it is checked whether the step is *)
|
ballarin@15076
|
211 |
(* valid. *)
|
ballarin@15076
|
212 |
(* *)
|
ballarin@15076
|
213 |
(* ******************************************************************* *)
|
ballarin@15076
|
214 |
|
ballarin@15076
|
215 |
fun transPath ([],acc) = acc
|
ballarin@15076
|
216 |
| transPath (x::xs,acc) = transPath (xs, makeStep(acc,x))
|
ballarin@15076
|
217 |
|
ballarin@15076
|
218 |
(* ********************************************************************* *)
|
ballarin@15076
|
219 |
(* Graph functions *)
|
ballarin@15076
|
220 |
(* ********************************************************************* *)
|
ballarin@15076
|
221 |
|
ballarin@15076
|
222 |
(* *********************************************************** *)
|
ballarin@15076
|
223 |
(* Functions for constructing graphs *)
|
ballarin@15076
|
224 |
(* *********************************************************** *)
|
ballarin@15076
|
225 |
|
ballarin@15076
|
226 |
fun addEdge (v,d,[]) = [(v,d)]
|
ballarin@15076
|
227 |
| addEdge (v,d,((u,dl)::el)) = if v aconv u then ((v,d@dl)::el)
|
ballarin@15076
|
228 |
else (u,dl):: (addEdge(v,d,el));
|
ballarin@15076
|
229 |
|
ballarin@15076
|
230 |
(* ********************************************************************** *)
|
ballarin@15076
|
231 |
(* *)
|
ballarin@15076
|
232 |
(* mkGraph constructs from a list of objects of type rel a graph g *)
|
ballarin@15098
|
233 |
(* and a list of all edges with label r+. *)
|
ballarin@15076
|
234 |
(* *)
|
ballarin@15076
|
235 |
(* ********************************************************************** *)
|
ballarin@15076
|
236 |
|
ballarin@15076
|
237 |
fun mkGraph [] = ([],[])
|
ballarin@15076
|
238 |
| mkGraph ys =
|
ballarin@15076
|
239 |
let
|
ballarin@15076
|
240 |
fun buildGraph ([],g,zs) = (g,zs)
|
ballarin@15076
|
241 |
| buildGraph (x::xs, g, zs) =
|
ballarin@15076
|
242 |
case x of (Trans (_,_,_)) =>
|
ballarin@15076
|
243 |
buildGraph (xs, addEdge((upper x), [],(addEdge ((lower x),[((upper x),x)],g))), x::zs)
|
ballarin@15076
|
244 |
| _ => buildGraph (xs, addEdge((upper x), [],(addEdge ((lower x),[((upper x),x)],g))), zs)
|
ballarin@15076
|
245 |
in buildGraph (ys, [], []) end;
|
ballarin@15076
|
246 |
|
ballarin@15076
|
247 |
(* *********************************************************************** *)
|
ballarin@15076
|
248 |
(* *)
|
ballarin@15076
|
249 |
(* adjacent g u : (''a * 'b list ) list -> ''a -> 'b list *)
|
ballarin@15076
|
250 |
(* *)
|
ballarin@15076
|
251 |
(* List of successors of u in graph g *)
|
ballarin@15076
|
252 |
(* *)
|
ballarin@15076
|
253 |
(* *********************************************************************** *)
|
ballarin@15076
|
254 |
|
ballarin@15076
|
255 |
fun adjacent eq_comp ((v,adj)::el) u =
|
ballarin@15076
|
256 |
if eq_comp (u, v) then adj else adjacent eq_comp el u
|
ballarin@15076
|
257 |
| adjacent _ [] _ = []
|
ballarin@15076
|
258 |
|
ballarin@15076
|
259 |
(* *********************************************************************** *)
|
ballarin@15076
|
260 |
(* *)
|
ballarin@15076
|
261 |
(* dfs eq_comp g u v: *)
|
ballarin@15076
|
262 |
(* ('a * 'a -> bool) -> ('a *( 'a * rel) list) list -> *)
|
ballarin@15076
|
263 |
(* 'a -> 'a -> (bool * ('a * rel) list) *)
|
ballarin@15076
|
264 |
(* *)
|
ballarin@15076
|
265 |
(* Depth first search of v from u. *)
|
ballarin@15076
|
266 |
(* Returns (true, path(u, v)) if successful, otherwise (false, []). *)
|
ballarin@15076
|
267 |
(* *)
|
ballarin@15076
|
268 |
(* *********************************************************************** *)
|
ballarin@15076
|
269 |
|
ballarin@15076
|
270 |
fun dfs eq_comp g u v =
|
ballarin@15076
|
271 |
let
|
ballarin@15076
|
272 |
val pred = ref nil;
|
ballarin@15076
|
273 |
val visited = ref nil;
|
ballarin@15076
|
274 |
|
ballarin@15076
|
275 |
fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
|
ballarin@15076
|
276 |
|
ballarin@15076
|
277 |
fun dfs_visit u' =
|
ballarin@15076
|
278 |
let val _ = visited := u' :: (!visited)
|
ballarin@15076
|
279 |
|
ballarin@15076
|
280 |
fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end;
|
ballarin@15076
|
281 |
|
ballarin@15076
|
282 |
in if been_visited v then ()
|
ballarin@15076
|
283 |
else (app (fn (v',l) => if been_visited v' then () else (
|
ballarin@15076
|
284 |
update (v',l);
|
ballarin@15076
|
285 |
dfs_visit v'; ()) )) (adjacent eq_comp g u')
|
ballarin@15076
|
286 |
end
|
ballarin@15076
|
287 |
in
|
ballarin@15076
|
288 |
dfs_visit u;
|
ballarin@15076
|
289 |
if (been_visited v) then (true, (!pred)) else (false , [])
|
ballarin@15076
|
290 |
end;
|
ballarin@15076
|
291 |
|
ballarin@15076
|
292 |
(* *********************************************************************** *)
|
ballarin@15076
|
293 |
(* *)
|
ballarin@15076
|
294 |
(* transpose g: *)
|
ballarin@15076
|
295 |
(* (''a * ''a list) list -> (''a * ''a list) list *)
|
ballarin@15076
|
296 |
(* *)
|
ballarin@15076
|
297 |
(* Computes transposed graph g' from g *)
|
ballarin@15076
|
298 |
(* by reversing all edges u -> v to v -> u *)
|
ballarin@15076
|
299 |
(* *)
|
ballarin@15076
|
300 |
(* *********************************************************************** *)
|
ballarin@15076
|
301 |
|
ballarin@15076
|
302 |
fun transpose eq_comp g =
|
ballarin@15076
|
303 |
let
|
ballarin@15076
|
304 |
(* Compute list of reversed edges for each adjacency list *)
|
ballarin@15076
|
305 |
fun flip (u,(v,l)::el) = (v,(u,l)) :: flip (u,el)
|
ballarin@15076
|
306 |
| flip (_,nil) = nil
|
ballarin@15076
|
307 |
|
ballarin@15076
|
308 |
(* Compute adjacency list for node u from the list of edges
|
ballarin@15076
|
309 |
and return a likewise reduced list of edges. The list of edges
|
ballarin@15076
|
310 |
is searches for edges starting from u, and these edges are removed. *)
|
ballarin@15076
|
311 |
fun gather (u,(v,w)::el) =
|
ballarin@15076
|
312 |
let
|
ballarin@15076
|
313 |
val (adj,edges) = gather (u,el)
|
ballarin@15076
|
314 |
in
|
ballarin@15076
|
315 |
if eq_comp (u, v) then (w::adj,edges)
|
ballarin@15076
|
316 |
else (adj,(v,w)::edges)
|
ballarin@15076
|
317 |
end
|
ballarin@15076
|
318 |
| gather (_,nil) = (nil,nil)
|
ballarin@15076
|
319 |
|
ballarin@15076
|
320 |
(* For every node in the input graph, call gather to find all reachable
|
ballarin@15076
|
321 |
nodes in the list of edges *)
|
ballarin@15076
|
322 |
fun assemble ((u,_)::el) edges =
|
ballarin@15076
|
323 |
let val (adj,edges) = gather (u,edges)
|
ballarin@15076
|
324 |
in (u,adj) :: assemble el edges
|
ballarin@15076
|
325 |
end
|
ballarin@15076
|
326 |
| assemble nil _ = nil
|
ballarin@15076
|
327 |
|
ballarin@15076
|
328 |
(* Compute, for each adjacency list, the list with reversed edges,
|
ballarin@15076
|
329 |
and concatenate these lists. *)
|
skalberg@15570
|
330 |
val flipped = Library.foldr (op @) ((map flip g),nil)
|
ballarin@15076
|
331 |
|
ballarin@15076
|
332 |
in assemble g flipped end
|
ballarin@15076
|
333 |
|
ballarin@15076
|
334 |
(* *********************************************************************** *)
|
ballarin@15076
|
335 |
(* *)
|
ballarin@15076
|
336 |
(* dfs_reachable eq_comp g u: *)
|
ballarin@15076
|
337 |
(* (int * int list) list -> int -> int list *)
|
ballarin@15076
|
338 |
(* *)
|
ballarin@15076
|
339 |
(* Computes list of all nodes reachable from u in g. *)
|
ballarin@15076
|
340 |
(* *)
|
ballarin@15076
|
341 |
(* *********************************************************************** *)
|
ballarin@15076
|
342 |
|
ballarin@15076
|
343 |
fun dfs_reachable eq_comp g u =
|
ballarin@15076
|
344 |
let
|
ballarin@15076
|
345 |
(* List of vertices which have been visited. *)
|
ballarin@15076
|
346 |
val visited = ref nil;
|
ballarin@15076
|
347 |
|
ballarin@15076
|
348 |
fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
|
ballarin@15076
|
349 |
|
ballarin@15076
|
350 |
fun dfs_visit g u =
|
ballarin@15076
|
351 |
let
|
ballarin@15076
|
352 |
val _ = visited := u :: !visited
|
ballarin@15076
|
353 |
val descendents =
|
skalberg@15570
|
354 |
Library.foldr (fn ((v,l),ds) => if been_visited v then ds
|
ballarin@15076
|
355 |
else v :: dfs_visit g v @ ds)
|
ballarin@15076
|
356 |
( ((adjacent eq_comp g u)) ,nil)
|
ballarin@15076
|
357 |
in descendents end
|
ballarin@15076
|
358 |
|
ballarin@15076
|
359 |
in u :: dfs_visit g u end;
|
ballarin@15076
|
360 |
|
ballarin@15076
|
361 |
(* *********************************************************************** *)
|
ballarin@15076
|
362 |
(* *)
|
ballarin@15076
|
363 |
(* dfs_term_reachable g u: *)
|
ballarin@15076
|
364 |
(* (term * term list) list -> term -> term list *)
|
ballarin@15076
|
365 |
(* *)
|
ballarin@15076
|
366 |
(* Computes list of all nodes reachable from u in g. *)
|
ballarin@15076
|
367 |
(* *)
|
ballarin@15076
|
368 |
(* *********************************************************************** *)
|
ballarin@15076
|
369 |
|
ballarin@15076
|
370 |
fun dfs_term_reachable g u = dfs_reachable (op aconv) g u;
|
ballarin@15076
|
371 |
|
ballarin@15076
|
372 |
(* ************************************************************************ *)
|
ballarin@15076
|
373 |
(* *)
|
ballarin@15076
|
374 |
(* findPath x y g: Term.term -> Term.term -> *)
|
ballarin@15076
|
375 |
(* (Term.term * (Term.term * rel list) list) -> *)
|
ballarin@15076
|
376 |
(* (bool, rel list) *)
|
ballarin@15076
|
377 |
(* *)
|
ballarin@15076
|
378 |
(* Searches a path from vertex x to vertex y in Graph g, returns true and *)
|
ballarin@15098
|
379 |
(* the list of edges if path is found, otherwise false and nil. *)
|
ballarin@15076
|
380 |
(* *)
|
ballarin@15076
|
381 |
(* ************************************************************************ *)
|
ballarin@15076
|
382 |
|
ballarin@15076
|
383 |
fun findPath x y g =
|
ballarin@15076
|
384 |
let
|
ballarin@15076
|
385 |
val (found, tmp) = dfs (op aconv) g x y ;
|
ballarin@15076
|
386 |
val pred = map snd tmp;
|
ballarin@15076
|
387 |
|
ballarin@15076
|
388 |
fun path x y =
|
ballarin@15076
|
389 |
let
|
ballarin@15076
|
390 |
(* find predecessor u of node v and the edge u -> v *)
|
ballarin@15076
|
391 |
|
ballarin@15076
|
392 |
fun lookup v [] = raise Cannot
|
ballarin@15076
|
393 |
| lookup v (e::es) = if (upper e) aconv v then e else lookup v es;
|
ballarin@15076
|
394 |
|
ballarin@15076
|
395 |
(* traverse path backwards and return list of visited edges *)
|
ballarin@15076
|
396 |
fun rev_path v =
|
ballarin@15076
|
397 |
let val l = lookup v pred
|
ballarin@15076
|
398 |
val u = lower l;
|
ballarin@15076
|
399 |
in
|
ballarin@15076
|
400 |
if u aconv x then [l] else (rev_path u) @ [l]
|
ballarin@15076
|
401 |
end
|
ballarin@15076
|
402 |
|
ballarin@15076
|
403 |
in rev_path y end;
|
ballarin@15076
|
404 |
|
ballarin@15076
|
405 |
in
|
ballarin@15076
|
406 |
|
ballarin@15076
|
407 |
|
ballarin@15076
|
408 |
if found then ( (found, (path x y) )) else (found,[])
|
ballarin@15076
|
409 |
|
ballarin@15076
|
410 |
|
ballarin@15076
|
411 |
|
ballarin@15076
|
412 |
end;
|
ballarin@15076
|
413 |
|
ballarin@15098
|
414 |
(* ************************************************************************ *)
|
ballarin@15098
|
415 |
(* *)
|
ballarin@15098
|
416 |
(* findRtranclProof g tranclEdges subgoal: *)
|
ballarin@15098
|
417 |
(* (Term.term * (Term.term * rel list) list) -> rel -> proof list *)
|
ballarin@15098
|
418 |
(* *)
|
ballarin@15098
|
419 |
(* Searches in graph g a proof for subgoal. *)
|
ballarin@15098
|
420 |
(* *)
|
ballarin@15098
|
421 |
(* ************************************************************************ *)
|
ballarin@15076
|
422 |
|
ballarin@15076
|
423 |
fun findRtranclProof g tranclEdges subgoal =
|
ballarin@15076
|
424 |
case subgoal of (RTrans (x,y,_)) => if x aconv y then [Thm ([], Cls.rtrancl_refl)] else (
|
ballarin@15076
|
425 |
let val (found, path) = findPath (lower subgoal) (upper subgoal) g
|
ballarin@15076
|
426 |
in
|
ballarin@15076
|
427 |
if found then (
|
ballarin@15076
|
428 |
let val path' = (transPath (tl path, hd path))
|
ballarin@15076
|
429 |
in
|
ballarin@15076
|
430 |
|
ballarin@15076
|
431 |
case path' of (Trans (_,_,p)) => [Thm ([p], Cls.trancl_into_rtrancl )]
|
ballarin@15076
|
432 |
| _ => [getprf path']
|
ballarin@15076
|
433 |
|
ballarin@15076
|
434 |
end
|
ballarin@15076
|
435 |
)
|
ballarin@15076
|
436 |
else raise Cannot
|
ballarin@15076
|
437 |
end
|
ballarin@15076
|
438 |
)
|
ballarin@15076
|
439 |
|
ballarin@15076
|
440 |
| (Trans (x,y,_)) => (
|
ballarin@15076
|
441 |
|
ballarin@15076
|
442 |
let
|
ballarin@15076
|
443 |
val Vx = dfs_term_reachable g x;
|
ballarin@15076
|
444 |
val g' = transpose (op aconv) g;
|
ballarin@15076
|
445 |
val Vy = dfs_term_reachable g' y;
|
ballarin@15076
|
446 |
|
ballarin@15076
|
447 |
fun processTranclEdges [] = raise Cannot
|
ballarin@15076
|
448 |
| processTranclEdges (e::es) =
|
ballarin@15076
|
449 |
if (upper e) mem Vx andalso (lower e) mem Vx
|
ballarin@15076
|
450 |
andalso (upper e) mem Vy andalso (lower e) mem Vy
|
ballarin@15076
|
451 |
then (
|
ballarin@15076
|
452 |
|
ballarin@15076
|
453 |
|
ballarin@15076
|
454 |
if (lower e) aconv x then (
|
ballarin@15076
|
455 |
if (upper e) aconv y then (
|
ballarin@15076
|
456 |
[(getprf e)]
|
ballarin@15076
|
457 |
)
|
ballarin@15076
|
458 |
else (
|
ballarin@15076
|
459 |
let
|
ballarin@15076
|
460 |
val (found,path) = findPath (upper e) y g
|
ballarin@15076
|
461 |
in
|
ballarin@15076
|
462 |
|
ballarin@15076
|
463 |
if found then (
|
ballarin@15076
|
464 |
[getprf (transPath (path, e))]
|
ballarin@15076
|
465 |
) else processTranclEdges es
|
ballarin@15076
|
466 |
|
ballarin@15076
|
467 |
end
|
ballarin@15076
|
468 |
)
|
ballarin@15076
|
469 |
)
|
ballarin@15076
|
470 |
else if (upper e) aconv y then (
|
ballarin@15076
|
471 |
let val (xufound,xupath) = findPath x (lower e) g
|
ballarin@15076
|
472 |
in
|
ballarin@15076
|
473 |
|
ballarin@15076
|
474 |
if xufound then (
|
ballarin@15076
|
475 |
|
ballarin@15076
|
476 |
let val xuRTranclEdge = transPath (tl xupath, hd xupath)
|
ballarin@15076
|
477 |
val xyTranclEdge = makeStep(xuRTranclEdge,e)
|
ballarin@15076
|
478 |
|
ballarin@15076
|
479 |
in [getprf xyTranclEdge] end
|
ballarin@15076
|
480 |
|
ballarin@15076
|
481 |
) else processTranclEdges es
|
ballarin@15076
|
482 |
|
ballarin@15076
|
483 |
end
|
ballarin@15076
|
484 |
)
|
ballarin@15076
|
485 |
else (
|
ballarin@15076
|
486 |
|
ballarin@15076
|
487 |
let val (xufound,xupath) = findPath x (lower e) g
|
ballarin@15076
|
488 |
val (vyfound,vypath) = findPath (upper e) y g
|
ballarin@15076
|
489 |
in
|
ballarin@15076
|
490 |
if xufound then (
|
ballarin@15076
|
491 |
if vyfound then (
|
ballarin@15076
|
492 |
let val xuRTranclEdge = transPath (tl xupath, hd xupath)
|
ballarin@15076
|
493 |
val vyRTranclEdge = transPath (tl vypath, hd vypath)
|
ballarin@15076
|
494 |
val xyTranclEdge = makeStep (makeStep(xuRTranclEdge,e),vyRTranclEdge)
|
ballarin@15076
|
495 |
|
ballarin@15076
|
496 |
in [getprf xyTranclEdge] end
|
ballarin@15076
|
497 |
|
ballarin@15076
|
498 |
) else processTranclEdges es
|
ballarin@15076
|
499 |
)
|
ballarin@15076
|
500 |
else processTranclEdges es
|
ballarin@15076
|
501 |
end
|
ballarin@15076
|
502 |
)
|
ballarin@15076
|
503 |
)
|
ballarin@15076
|
504 |
else processTranclEdges es;
|
ballarin@15076
|
505 |
in processTranclEdges tranclEdges end )
|
ballarin@15076
|
506 |
| _ => raise Cannot
|
ballarin@15076
|
507 |
|
ballarin@15076
|
508 |
|
ballarin@15076
|
509 |
fun solveTrancl (asms, concl) =
|
ballarin@15076
|
510 |
let val (g,_) = mkGraph asms
|
ballarin@15076
|
511 |
in
|
ballarin@15076
|
512 |
let val (_, subgoal, _) = mkconcl_trancl concl
|
ballarin@15076
|
513 |
val (found, path) = findPath (lower subgoal) (upper subgoal) g
|
ballarin@15076
|
514 |
in
|
ballarin@15076
|
515 |
if found then [getprf (transPath (tl path, hd path))]
|
ballarin@15076
|
516 |
else raise Cannot
|
ballarin@15076
|
517 |
end
|
ballarin@15076
|
518 |
end;
|
ballarin@15076
|
519 |
|
ballarin@15076
|
520 |
fun solveRtrancl (asms, concl) =
|
ballarin@15076
|
521 |
let val (g,tranclEdges) = mkGraph asms
|
ballarin@15076
|
522 |
val (_, subgoal, _) = mkconcl_rtrancl concl
|
ballarin@15076
|
523 |
in
|
ballarin@15076
|
524 |
findRtranclProof g tranclEdges subgoal
|
ballarin@15076
|
525 |
end;
|
ballarin@15076
|
526 |
|
ballarin@15076
|
527 |
|
ballarin@15076
|
528 |
val trancl_tac = SUBGOAL (fn (A, n) =>
|
ballarin@15076
|
529 |
let
|
ballarin@15076
|
530 |
val Hs = Logic.strip_assums_hyp A;
|
ballarin@15076
|
531 |
val C = Logic.strip_assums_concl A;
|
ballarin@15076
|
532 |
val (rel,subgoals, prf) = mkconcl_trancl C;
|
skalberg@15570
|
533 |
val prems = List.concat (ListPair.map (mkasm_trancl rel) (Hs, 0 upto (length Hs - 1)))
|
ballarin@15076
|
534 |
val prfs = solveTrancl (prems, C);
|
ballarin@15076
|
535 |
|
ballarin@15076
|
536 |
in
|
ballarin@15076
|
537 |
METAHYPS (fn asms =>
|
ballarin@15076
|
538 |
let val thms = map (prove asms) prfs
|
ballarin@15076
|
539 |
in rtac (prove thms prf) 1 end) n
|
ballarin@15076
|
540 |
end
|
ballarin@15076
|
541 |
handle Cannot => no_tac);
|
ballarin@15076
|
542 |
|
ballarin@15076
|
543 |
|
ballarin@15076
|
544 |
|
ballarin@15076
|
545 |
val rtrancl_tac = SUBGOAL (fn (A, n) =>
|
ballarin@15076
|
546 |
let
|
ballarin@15076
|
547 |
val Hs = Logic.strip_assums_hyp A;
|
ballarin@15076
|
548 |
val C = Logic.strip_assums_concl A;
|
ballarin@15076
|
549 |
val (rel,subgoals, prf) = mkconcl_rtrancl C;
|
ballarin@15076
|
550 |
|
skalberg@15570
|
551 |
val prems = List.concat (ListPair.map (mkasm_rtrancl rel) (Hs, 0 upto (length Hs - 1)))
|
ballarin@15076
|
552 |
val prfs = solveRtrancl (prems, C);
|
ballarin@15076
|
553 |
in
|
ballarin@15076
|
554 |
METAHYPS (fn asms =>
|
ballarin@15076
|
555 |
let val thms = map (prove asms) prfs
|
ballarin@15076
|
556 |
in rtac (prove thms prf) 1 end) n
|
ballarin@15076
|
557 |
end
|
ballarin@15076
|
558 |
handle Cannot => no_tac);
|
ballarin@15076
|
559 |
|
ballarin@15076
|
560 |
end;
|