|
1 (* |
|
2 Title: Transitivity reasoner for partial and linear orders |
|
3 Id: $Id$ |
|
4 Author: Oliver Kutter |
|
5 Copyright: TU Muenchen |
|
6 *) |
|
7 |
|
8 (* TODO: reduce number of input thms, reduce code duplication *) |
|
9 |
|
10 (* |
|
11 |
|
12 The packages provides tactics partial_tac and linear_tac that use all |
|
13 premises of the form |
|
14 |
|
15 t = u, t ~= u, t < u, t <= u, ~(t < u) and ~(t <= u) |
|
16 |
|
17 to |
|
18 1. either derive a contradiction, |
|
19 in which case the conclusion can be any term, |
|
20 2. or prove the conclusion, which must be of the same form as the |
|
21 premises (excluding ~(t < u) and ~(t <= u) for partial orders) |
|
22 |
|
23 The package is implemented as an ML functor and thus not limited to the |
|
24 relation <= and friends. It can be instantiated to any partial and/or |
|
25 linear order --- for example, the divisibility relation "dvd". In |
|
26 order to instantiate the package for a partial order only, supply |
|
27 dummy theorems to the rules for linear orders, and don't use |
|
28 linear_tac! |
|
29 |
|
30 *) |
|
31 |
|
32 signature LESS_ARITH = |
|
33 sig |
|
34 (* Theorems for partial orders *) |
|
35 val less_reflE: thm (* x < x ==> P *) |
|
36 val le_refl: thm (* x <= x *) |
|
37 val less_imp_le: thm (* x < y ==> x <= y *) |
|
38 val eqI: thm (* [| x <= y; y <= x |] ==> x = y *) |
|
39 val eqD1: thm (* x = y ==> x <= y *) |
|
40 val eqD2: thm (* x = y ==> y <= x *) |
|
41 val less_trans: thm (* [| x <= y; y <= z |] ==> x <= z *) |
|
42 val less_le_trans: thm (* [| x <= y; y < z |] ==> x < z *) |
|
43 val le_less_trans: thm (* [| x < y; y <= z |] ==> x < z *) |
|
44 val le_trans: thm (* [| x < y; y < z |] ==> x < z *) |
|
45 val le_neq_trans : thm (* [| x <= y ; x ~= y |] ==> x < y *) |
|
46 val neq_le_trans : thm (* [| x ~= y ; x <= y |] ==> x < y *) |
|
47 |
|
48 (* Additional theorems for linear orders *) |
|
49 val not_lessD: thm (* ~(x < y) ==> y <= x *) |
|
50 val not_leD: thm (* ~(x <= y) ==> y < x *) |
|
51 val not_lessI: thm (* y <= x ==> ~(x < y) *) |
|
52 val not_leI: thm (* y < x ==> ~(x <= y) *) |
|
53 |
|
54 (* Additional theorems for subgoals of form x ~= y *) |
|
55 val less_imp_neq : thm (* x < y ==> x ~= y *) |
|
56 val eq_neq_eq_imp_neq : thm (* [| x = u ; u ~= v ; v = z|] ==> x ~= z *) |
|
57 |
|
58 (* Analysis of premises and conclusion *) |
|
59 (* decomp_x (`x Rel y') should yield (x, Rel, y) |
|
60 where Rel is one of "<", "<=", "~<", "~<=", "=" and "~=", |
|
61 other relation symbols cause an error message *) |
|
62 val decomp_part: Sign.sg -> term -> (term * string * term) option |
|
63 val decomp_lin: Sign.sg -> term -> (term * string * term) option |
|
64 end; |
|
65 |
|
66 signature TRANS_TAC = |
|
67 sig |
|
68 val partial_tac: int -> tactic |
|
69 val linear_tac: int -> tactic |
|
70 end; |
|
71 |
|
72 functor Trans_Tac_Fun (Less: LESS_ARITH): TRANS_TAC = |
|
73 struct |
|
74 |
|
75 (* Extract subgoal with signature *) |
|
76 |
|
77 fun SUBGOAL goalfun i st = |
|
78 goalfun (List.nth(prems_of st, i-1), i, sign_of_thm st) st |
|
79 handle Subscript => Seq.empty; |
|
80 |
|
81 (* Internal datatype for the proof *) |
|
82 datatype proof |
|
83 = Asm of int |
|
84 | Thm of proof list * thm; |
|
85 |
|
86 exception Cannot; |
|
87 (* Internal exception, raised if conclusion cannot be derived from |
|
88 assumptions. *) |
|
89 exception Contr of proof; |
|
90 (* Internal exception, raised if contradiction ( x < x ) was derived *) |
|
91 |
|
92 fun prove asms = |
|
93 let fun pr (Asm i) = nth_elem (i, asms) |
|
94 | pr (Thm (prfs, thm)) = (map pr prfs) MRS thm |
|
95 in pr end; |
|
96 |
|
97 (* Internal datatype for inequalities *) |
|
98 datatype less |
|
99 = Less of term * term * proof |
|
100 | Le of term * term * proof |
|
101 | NotEq of term * term * proof; |
|
102 |
|
103 |
|
104 (* Misc functions for datatype less *) |
|
105 fun lower (Less (x, _, _)) = x |
|
106 | lower (Le (x, _, _)) = x |
|
107 | lower (NotEq (x,_,_)) = x; |
|
108 |
|
109 fun upper (Less (_, y, _)) = y |
|
110 | upper (Le (_, y, _)) = y |
|
111 | upper (NotEq (_,y,_)) = y; |
|
112 |
|
113 fun getprf (Less (_, _, p)) = p |
|
114 | getprf (Le (_, _, p)) = p |
|
115 | getprf (NotEq (_,_, p)) = p; |
|
116 |
|
117 |
|
118 (* ************************************************************************ *) |
|
119 (* *) |
|
120 (* mkasm_partial sign (t, n) : Sign.sg -> (Term.term * int) -> less *) |
|
121 (* *) |
|
122 (* Tuple (t, n) (t an assumption, n its index in the assumptions) is *) |
|
123 (* translated to an element of type less. *) |
|
124 (* Partial orders only. *) |
|
125 (* *) |
|
126 (* ************************************************************************ *) |
|
127 |
|
128 fun mkasm_partial sign (t, n) = |
|
129 case Less.decomp_part sign t of |
|
130 Some (x, rel, y) => (case rel of |
|
131 "<" => if (x aconv y) then raise Contr (Thm ([Asm n], Less.less_reflE)) |
|
132 else [Less (x, y, Asm n)] |
|
133 | "~<" => [] |
|
134 | "<=" => [Le (x, y, Asm n)] |
|
135 | "~<=" => [] |
|
136 | "=" => [Le (x, y, Thm ([Asm n], Less.eqD1)), |
|
137 Le (y, x, Thm ([Asm n], Less.eqD2))] |
|
138 | "~=" => if (x aconv y) then |
|
139 raise Contr (Thm ([(Thm ([(Thm ([], Less.le_refl)) ,(Asm n)], Less.le_neq_trans))], Less.less_reflE)) |
|
140 else [ NotEq (x, y, Asm n), |
|
141 NotEq (y, x,Thm ( [Asm n], thm "not_sym"))] (* Le (x, x, Thm ([],Less.le_refl))]*) |
|
142 | _ => error ("partial_tac: unknown relation symbol ``" ^ rel ^ |
|
143 "''returned by decomp_part.")) |
|
144 | None => []; |
|
145 |
|
146 |
|
147 |
|
148 (* ************************************************************************ *) |
|
149 (* *) |
|
150 (* mkasm_linear sign (t, n) : Sign.sg -> (Term.term * int) -> less *) |
|
151 (* *) |
|
152 (* Tuple (t, n) (t an assumption, n its index in the assumptions) is *) |
|
153 (* translated to an element of type less. *) |
|
154 (* Linear orders only. *) |
|
155 (* *) |
|
156 (* ************************************************************************ *) |
|
157 |
|
158 fun mkasm_linear sign (t, n) = |
|
159 case Less.decomp_lin sign t of |
|
160 Some (x, rel, y) => (case rel of |
|
161 "<" => if (x aconv y) then raise Contr (Thm ([Asm n], Less.less_reflE)) |
|
162 else [Less (x, y, Asm n)] |
|
163 | "~<" => [Le (y, x, Thm ([Asm n], Less.not_lessD))] |
|
164 | "<=" => [Le (x, y, Asm n)] |
|
165 | "~<=" => if (x aconv y) then |
|
166 raise (Contr (Thm ([Thm ([Asm n], Less.not_leD)], Less.less_reflE))) |
|
167 else [Less (y, x, Thm ([Asm n], Less.not_leD))] |
|
168 | "=" => [Le (x, y, Thm ([Asm n], Less.eqD1)), |
|
169 Le (y, x, Thm ([Asm n], Less.eqD2))] |
|
170 | "~=" => if (x aconv y) then |
|
171 raise Contr (Thm ([(Thm ([(Thm ([], Less.le_refl)) ,(Asm n)], Less.le_neq_trans))], Less.less_reflE)) |
|
172 else [ NotEq (x, y, Asm n), |
|
173 NotEq (y, x,Thm ( [Asm n], thm "not_sym"))] |
|
174 | _ => error ("linear_tac: unknown relation symbol ``" ^ rel ^ |
|
175 "''returned by decomp_lin.")) |
|
176 | None => []; |
|
177 |
|
178 |
|
179 (* ************************************************************************ *) |
|
180 (* *) |
|
181 (* mkconcl_partial sign t : Sign.sg -> Term.term -> less *) |
|
182 (* *) |
|
183 (* Translates conclusion t to an element of type less. *) |
|
184 (* Partial orders only. *) |
|
185 (* *) |
|
186 (* ************************************************************************ *) |
|
187 |
|
188 fun mkconcl_partial sign t = |
|
189 case Less.decomp_part sign t of |
|
190 Some (x, rel, y) => (case rel of |
|
191 "<" => ([Less (x, y, Asm ~1)], Asm 0) |
|
192 | "<=" => ([Le (x, y, Asm ~1)], Asm 0) |
|
193 | "=" => ([Le (x, y, Asm ~1), Le (y, x, Asm ~1)], |
|
194 Thm ([Asm 0, Asm 1], Less.eqI)) |
|
195 | "~=" => ([NotEq (x,y, Asm ~1)], Asm 0) |
|
196 | _ => raise Cannot) |
|
197 | None => raise Cannot; |
|
198 |
|
199 |
|
200 (* ************************************************************************ *) |
|
201 (* *) |
|
202 (* mkconcl_linear sign t : Sign.sg -> Term.term -> less *) |
|
203 (* *) |
|
204 (* Translates conclusion t to an element of type less. *) |
|
205 (* Linear orders only. *) |
|
206 (* *) |
|
207 (* ************************************************************************ *) |
|
208 |
|
209 fun mkconcl_linear sign t = |
|
210 case Less.decomp_lin sign t of |
|
211 Some (x, rel, y) => (case rel of |
|
212 "<" => ([Less (x, y, Asm ~1)], Asm 0) |
|
213 | "~<" => ([Le (y, x, Asm ~1)], Thm ([Asm 0], Less.not_lessI)) |
|
214 | "<=" => ([Le (x, y, Asm ~1)], Asm 0) |
|
215 | "~<=" => ([Less (y, x, Asm ~1)], Thm ([Asm 0], Less.not_leI)) |
|
216 | "=" => ([Le (x, y, Asm ~1), Le (y, x, Asm ~1)], |
|
217 Thm ([Asm 0, Asm 1], Less.eqI)) |
|
218 | "~=" => ([NotEq (x,y, Asm ~1)], Asm 0) |
|
219 | _ => raise Cannot) |
|
220 | None => raise Cannot; |
|
221 |
|
222 |
|
223 |
|
224 (* ******************************************************************* *) |
|
225 (* *) |
|
226 (* mergeLess (less1,less2): less * less -> less *) |
|
227 (* *) |
|
228 (* Merge to elements of type less according to the following rules *) |
|
229 (* *) |
|
230 (* x < y && y < z ==> x < z *) |
|
231 (* x < y && y <= z ==> x < z *) |
|
232 (* x <= y && y < z ==> x < z *) |
|
233 (* x <= y && y <= z ==> x <= z *) |
|
234 (* x <= y && x ~= y ==> x < y *) |
|
235 (* x ~= y && x <= y ==> x < y *) |
|
236 (* x < y && x ~= y ==> x < y *) |
|
237 (* x ~= y && x < y ==> x < y *) |
|
238 (* *) |
|
239 (* ******************************************************************* *) |
|
240 |
|
241 fun mergeLess (Less (x, _, p) , Less (_ , z, q)) = |
|
242 Less (x, z, Thm ([p,q] , Less.less_trans)) |
|
243 | mergeLess (Less (x, _, p) , Le (_ , z, q)) = |
|
244 Less (x, z, Thm ([p,q] , Less.less_le_trans)) |
|
245 | mergeLess (Le (x, _, p) , Less (_ , z, q)) = |
|
246 Less (x, z, Thm ([p,q] , Less.le_less_trans)) |
|
247 | mergeLess (Le (x, z, p) , NotEq (x', z', q)) = |
|
248 if (x aconv x' andalso z aconv z' ) |
|
249 then Less (x, z, Thm ([p,q] , Less.le_neq_trans)) |
|
250 else error "linear/partial_tac: internal error le_neq_trans" |
|
251 | mergeLess (NotEq (x, z, p) , Le (x' , z', q)) = |
|
252 if (x aconv x' andalso z aconv z') |
|
253 then Less (x, z, Thm ([p,q] , Less.neq_le_trans)) |
|
254 else error "linear/partial_tac: internal error neq_le_trans" |
|
255 | mergeLess (NotEq (x, z, p) , Less (x' , z', q)) = |
|
256 if (x aconv x' andalso z aconv z') |
|
257 then Less ((x' , z', q)) |
|
258 else error "linear/partial_tac: internal error neq_less_trans" |
|
259 | mergeLess (Less (x, z, p) , NotEq (x', z', q)) = |
|
260 if (x aconv x' andalso z aconv z') |
|
261 then Less (x, z, p) |
|
262 else error "linear/partial_tac: internal error less_neq_trans" |
|
263 | mergeLess (Le (x, _, p) , Le (_ , z, q)) = |
|
264 Le (x, z, Thm ([p,q] , Less.le_trans)) |
|
265 | mergeLess (_, _) = |
|
266 error "linear/partial_tac: internal error: undefined case"; |
|
267 |
|
268 |
|
269 (* ******************************************************************** *) |
|
270 (* tr checks for valid transitivity step *) |
|
271 (* ******************************************************************** *) |
|
272 |
|
273 infix tr; |
|
274 fun (Less (_, y, _)) tr (Le (x', _, _)) = ( y aconv x' ) |
|
275 | (Le (_, y, _)) tr (Less (x', _, _)) = ( y aconv x' ) |
|
276 | (Less (_, y, _)) tr (Less (x', _, _)) = ( y aconv x' ) |
|
277 | (Le (_, y, _)) tr (Le (x', _, _)) = ( y aconv x' ) |
|
278 | _ tr _ = false; |
|
279 |
|
280 |
|
281 (* ******************************************************************* *) |
|
282 (* *) |
|
283 (* transPath (Lesslist, Less): (less list * less) -> less *) |
|
284 (* *) |
|
285 (* If a path represented by a list of elements of type less is found, *) |
|
286 (* this needs to be contracted to a single element of type less. *) |
|
287 (* Prior to each transitivity step it is checked whether the step is *) |
|
288 (* valid. *) |
|
289 (* *) |
|
290 (* ******************************************************************* *) |
|
291 |
|
292 fun transPath ([],lesss) = lesss |
|
293 | transPath (x::xs,lesss) = |
|
294 if lesss tr x then transPath (xs, mergeLess(lesss,x)) |
|
295 else error "linear/partial_tac: internal error transpath"; |
|
296 |
|
297 (* ******************************************************************* *) |
|
298 (* *) |
|
299 (* less1 subsumes less2 : less -> less -> bool *) |
|
300 (* *) |
|
301 (* subsumes checks whether less1 implies less2 *) |
|
302 (* *) |
|
303 (* ******************************************************************* *) |
|
304 |
|
305 infix subsumes; |
|
306 fun (Less (x, y, _)) subsumes (Le (x', y', _)) = |
|
307 (x aconv x' andalso y aconv y') |
|
308 | (Less (x, y, _)) subsumes (Less (x', y', _)) = |
|
309 (x aconv x' andalso y aconv y') |
|
310 | (Le (x, y, _)) subsumes (Le (x', y', _)) = |
|
311 (x aconv x' andalso y aconv y') |
|
312 | (Less (x, y, _)) subsumes (NotEq (x', y', _)) = |
|
313 (x aconv x' andalso y aconv y') orelse (y aconv x' andalso x aconv y') |
|
314 | (NotEq (x, y, _)) subsumes (NotEq (x', y', _)) = |
|
315 (x aconv x' andalso y aconv y') orelse (y aconv x' andalso x aconv y') |
|
316 | (Le _) subsumes (Less _) = |
|
317 error "linear/partial_tac: internal error: Le cannot subsume Less" |
|
318 | _ subsumes _ = false; |
|
319 |
|
320 (* ******************************************************************* *) |
|
321 (* *) |
|
322 (* triv_solv less1 : less -> proof Library.option *) |
|
323 (* *) |
|
324 (* Solves trivial goal x <= x. *) |
|
325 (* *) |
|
326 (* ******************************************************************* *) |
|
327 |
|
328 fun triv_solv (Le (x, x', _)) = |
|
329 if x aconv x' then Some (Thm ([], Less.le_refl)) |
|
330 else None |
|
331 | triv_solv _ = None; |
|
332 |
|
333 (* ********************************************************************* *) |
|
334 (* Graph functions *) |
|
335 (* ********************************************************************* *) |
|
336 |
|
337 |
|
338 |
|
339 (* ******************************************************************* *) |
|
340 (* *) |
|
341 (* General: *) |
|
342 (* *) |
|
343 (* Inequalities are represented by various types of graphs. *) |
|
344 (* *) |
|
345 (* 1. (Term.term * Term.term list) list *) |
|
346 (* - Graph of this type is generated from the assumptions, *) |
|
347 (* does not contain information on which edge stems from which *) |
|
348 (* assumption. *) |
|
349 (* - Used to compute strong components. *) |
|
350 (* *) |
|
351 (* 2. (Term.term * (Term.term * less) list) list *) |
|
352 (* - Graph of this type is generated from the assumptions, *) |
|
353 (* it does contain information on which edge stems from which *) |
|
354 (* assumption. *) |
|
355 (* - Used to reconstruct paths. *) |
|
356 (* *) |
|
357 (* 3. (int * (int * less) list ) list *) |
|
358 (* - Graph of this type is generated from the strong components of *) |
|
359 (* graph of type 2. It consists of the strong components of *) |
|
360 (* graph 2, where nodes are indices of the components. *) |
|
361 (* Only edges between components are part of this graph. *) |
|
362 (* - Used to reconstruct paths between several components. *) |
|
363 (* *) |
|
364 (* 4. (int * int list) list *) |
|
365 (* - Graph of this type is generated from graph of type 3, but *) |
|
366 (* edge information of type less is removed. *) |
|
367 (* - Used to *) |
|
368 (* - Compute transposed graphs of type 4. *) |
|
369 (* - Compute list of components reachable from a component. *) |
|
370 (* *) |
|
371 (* *) |
|
372 (* ******************************************************************* *) |
|
373 |
|
374 |
|
375 (* *********************************************************** *) |
|
376 (* Functions for constructing graphs *) |
|
377 (* *********************************************************** *) |
|
378 |
|
379 fun addLessEdge (v,d,[]) = [(v,d)] |
|
380 | addLessEdge (v,d,((u,dl)::el)) = if v aconv u then ((v,d@dl)::el) |
|
381 else (u,dl):: (addLessEdge(v,d,el)); |
|
382 |
|
383 fun addTermEdge (v,u,[]) = [(v,[u])] |
|
384 | addTermEdge (v,u,((x,adj)::el)) = if v aconv x then (v,u::adj)::el |
|
385 else (x,adj) :: addTermEdge (v,u,el); |
|
386 |
|
387 (* ********************************************************************* *) |
|
388 (* *) |
|
389 (* buildGraphs constructs three graphs from a list of type less: *) |
|
390 (* g1: graph for the <= relation *) |
|
391 (* g2: graph for the <= relation with additional information for *) |
|
392 (* proof reconstruction *) |
|
393 (* neqEdges: all edges that are candidates for a ~= *) |
|
394 (* *) |
|
395 (* ********************************************************************* *) |
|
396 |
|
397 |
|
398 fun buildGraphs ([],g1,g2,neqEdges) = (g1, g2, neqEdges) |
|
399 | buildGraphs (l::ls,g1,g2,neqEdges) = case l of |
|
400 (Less (x,y,p)) =>( |
|
401 let val g1' = addTermEdge (x,y,g1) |
|
402 and g2' = addLessEdge (x,[(y,(Less (x, y, p)))],g2) |
|
403 in buildGraphs (ls,g1',g2',l::neqEdges) end) |
|
404 | (Le (x,y,p)) => |
|
405 ( let val g1' = addTermEdge (x,y,g1) |
|
406 and g2' = addLessEdge (x,[(y,(Le (x, y,p)))],g2) |
|
407 in buildGraphs (ls,g1',g2',neqEdges) end) |
|
408 | (NotEq (x,y,p)) => ( buildGraphs (ls,g1,g2,l::neqEdges) ) |
|
409 |
|
410 |
|
411 (* *********************************************************************** *) |
|
412 (* *) |
|
413 (* adjacent_term g u : (Term.term * 'a list ) list -> Term.term -> 'a list *) |
|
414 (* *) |
|
415 (* *) |
|
416 (* *********************************************************************** *) |
|
417 |
|
418 fun adjacent_term ((v,adj)::el) u = |
|
419 if u aconv v then adj else adjacent_term el u |
|
420 | adjacent_term nil _ = [] |
|
421 |
|
422 (* *********************************************************************** *) |
|
423 (* *) |
|
424 (* adjacent_term g u : (''a * 'b list ) list -> ''a -> 'b list *) |
|
425 (* *) |
|
426 (* List of successors of u in graph g *) |
|
427 (* *) |
|
428 (* *********************************************************************** *) |
|
429 |
|
430 fun adjacent ((v,adj)::el) u = |
|
431 if u = v then adj else adjacent el u |
|
432 | adjacent nil _ = [] |
|
433 |
|
434 |
|
435 (* *********************************************************************** *) |
|
436 (* *) |
|
437 (* transpose_term g: *) |
|
438 (* (Term.term * Term.term list) list -> (Term.term * Term.term list) list *) |
|
439 (* *) |
|
440 (* Computes transposed graph g' from g *) |
|
441 (* by reversing all edges u -> v to v -> u *) |
|
442 (* *) |
|
443 (* *********************************************************************** *) |
|
444 |
|
445 fun transpose_term g = |
|
446 let |
|
447 (* Compute list of reversed edges for each adjacency list *) |
|
448 fun flip (u,v::el) = (v,u) :: flip (u,el) |
|
449 | flip (_,nil) = nil |
|
450 |
|
451 (* Compute adjacency list for node u from the list of edges |
|
452 and return a likewise reduced list of edges. The list of edges |
|
453 is searches for edges starting from u, and these edges are removed. *) |
|
454 fun gather (u,(v,w)::el) = |
|
455 let |
|
456 val (adj,edges) = gather (u,el) |
|
457 in |
|
458 if u aconv v then (w::adj,edges) |
|
459 else (adj,(v,w)::edges) |
|
460 end |
|
461 | gather (_,nil) = (nil,nil) |
|
462 |
|
463 (* For every node in the input graph, call gather to find all reachable |
|
464 nodes in the list of edges *) |
|
465 fun assemble ((u,_)::el) edges = |
|
466 let val (adj,edges) = gather (u,edges) |
|
467 in (u,adj) :: assemble el edges |
|
468 end |
|
469 | assemble nil _ = nil |
|
470 |
|
471 (* Compute, for each adjacency list, the list with reversed edges, |
|
472 and concatenate these lists. *) |
|
473 val flipped = foldr (op @) ((map flip g),nil) |
|
474 |
|
475 in assemble g flipped end |
|
476 |
|
477 (* *********************************************************************** *) |
|
478 (* *) |
|
479 (* transpose g: *) |
|
480 (* (''a * ''a list) list -> (''a * ''a list) list *) |
|
481 (* *) |
|
482 (* Computes transposed graph g' from g *) |
|
483 (* by reversing all edges u -> v to v -> u *) |
|
484 (* *) |
|
485 (* *********************************************************************** *) |
|
486 |
|
487 fun transpose g = |
|
488 let |
|
489 (* Compute list of reversed edges for each adjacency list *) |
|
490 fun flip (u,v::el) = (v,u) :: flip (u,el) |
|
491 | flip (_,nil) = nil |
|
492 |
|
493 (* Compute adjacency list for node u from the list of edges |
|
494 and return a likewise reduced list of edges. The list of edges |
|
495 is searches for edges starting from u, and these edges are removed. *) |
|
496 fun gather (u,(v,w)::el) = |
|
497 let |
|
498 val (adj,edges) = gather (u,el) |
|
499 in |
|
500 if u = v then (w::adj,edges) |
|
501 else (adj,(v,w)::edges) |
|
502 end |
|
503 | gather (_,nil) = (nil,nil) |
|
504 |
|
505 (* For every node in the input graph, call gather to find all reachable |
|
506 nodes in the list of edges *) |
|
507 fun assemble ((u,_)::el) edges = |
|
508 let val (adj,edges) = gather (u,edges) |
|
509 in (u,adj) :: assemble el edges |
|
510 end |
|
511 | assemble nil _ = nil |
|
512 |
|
513 (* Compute, for each adjacency list, the list with reversed edges, |
|
514 and concatenate these lists. *) |
|
515 val flipped = foldr (op @) ((map flip g),nil) |
|
516 |
|
517 in assemble g flipped end |
|
518 |
|
519 |
|
520 (* scc_term : (term * term list) list -> term list list *) |
|
521 |
|
522 (* The following is based on the algorithm for finding strongly |
|
523 connected components described in Introduction to Algorithms, |
|
524 by Cormon, Leiserson, and Rivest, section 23.5. The input G |
|
525 is an adjacency list description of a directed graph. The |
|
526 output is a list of the strongly connected components (each a |
|
527 list of vertices). *) |
|
528 |
|
529 fun scc_term G = |
|
530 let |
|
531 (* Ordered list of the vertices that DFS has finished with; |
|
532 most recently finished goes at the head. *) |
|
533 val finish : term list ref = ref nil |
|
534 |
|
535 (* List of vertices which have been visited. *) |
|
536 val visited : term list ref = ref nil |
|
537 |
|
538 fun been_visited v = exists (fn w => w aconv v) (!visited) |
|
539 |
|
540 (* Given the adjacency list rep of a graph (a list of pairs), |
|
541 return just the first element of each pair, yielding the |
|
542 vertex list. *) |
|
543 val members = map (fn (v,_) => v) |
|
544 |
|
545 (* Returns the nodes in the DFS tree rooted at u in g *) |
|
546 fun dfs_visit g u : term list = |
|
547 let |
|
548 val _ = visited := u :: !visited |
|
549 val descendents = |
|
550 foldr (fn (v,ds) => if been_visited v then ds |
|
551 else v :: dfs_visit g v @ ds) |
|
552 ((adjacent_term g u) ,nil) |
|
553 in |
|
554 finish := u :: !finish; |
|
555 descendents |
|
556 end |
|
557 in |
|
558 |
|
559 (* DFS on the graph; apply dfs_visit to each vertex in |
|
560 the graph, checking first to make sure the vertex is |
|
561 as yet unvisited. *) |
|
562 app (fn u => if been_visited u then () |
|
563 else (dfs_visit G u; ())) (members G); |
|
564 visited := nil; |
|
565 |
|
566 (* We don't reset finish because its value is used by |
|
567 revfold below, and it will never be used again (even |
|
568 though dfs_visit will continue to modify it). *) |
|
569 |
|
570 (* DFS on the transpose. The vertices returned by |
|
571 dfs_visit along with u form a connected component. We |
|
572 collect all the connected components together in a |
|
573 list, which is what is returned. *) |
|
574 foldl (fn (comps,u) => |
|
575 if been_visited u then comps |
|
576 else ((u :: dfs_visit (transpose_term G) u) :: comps)) (nil,(!finish)) |
|
577 end; |
|
578 |
|
579 |
|
580 (* *********************************************************************** *) |
|
581 (* *) |
|
582 (* dfs_int_reachable g u: *) |
|
583 (* (int * int list) list -> int -> int list *) |
|
584 (* *) |
|
585 (* Computes list of all nodes reachable from u in g. *) |
|
586 (* *) |
|
587 (* *********************************************************************** *) |
|
588 |
|
589 |
|
590 fun dfs_int_reachable g u = |
|
591 let |
|
592 (* List of vertices which have been visited. *) |
|
593 val visited : int list ref = ref nil |
|
594 |
|
595 fun been_visited v = exists (fn w => w = v) (!visited) |
|
596 |
|
597 fun dfs_visit g u : int list = |
|
598 let |
|
599 val _ = visited := u :: !visited |
|
600 val descendents = |
|
601 foldr (fn (v,ds) => if been_visited v then ds |
|
602 else v :: dfs_visit g v @ ds) |
|
603 ( ((adjacent g u)) ,nil) |
|
604 in descendents end |
|
605 |
|
606 in u :: dfs_visit g u end; |
|
607 |
|
608 |
|
609 fun indexComps components = |
|
610 ListPair.map (fn (a,b) => (b,a)) (components, 0 upto (length components -1)); |
|
611 |
|
612 fun indexNodes IndexComp = |
|
613 flat (map (fn (index, comp) => (map (fn v => (v,index)) comp)) IndexComp); |
|
614 |
|
615 fun getIndex v [] = ~1 |
|
616 | getIndex v ((v',k)::vs) = if v aconv v' then k else getIndex v vs; |
|
617 |
|
618 |
|
619 (* ***************************************************************** *) |
|
620 (* *) |
|
621 (* evalcompgraph components g ntc : *) |
|
622 (* Term.term list list -> *) |
|
623 (* (Term.term * (Term.term * less) list) list -> *) |
|
624 (* (Term.term * int) list -> (int * (int * less) list) list *) |
|
625 (* *) |
|
626 (* *) |
|
627 (* Computes, from graph g, list of all its components and the list *) |
|
628 (* ntc (nodes, index of component) a graph whose nodes are the *) |
|
629 (* indices of the components of g. Egdes of the new graph are *) |
|
630 (* only the edges of g linking two components. *) |
|
631 (* *) |
|
632 (* ***************************************************************** *) |
|
633 |
|
634 fun evalcompgraph components g ntc = |
|
635 let |
|
636 (* Liste (Index der Komponente, Komponente *) |
|
637 val IndexComp = indexComps components; |
|
638 |
|
639 (* Compute new graph with the property that it only contains edges |
|
640 between components. *) |
|
641 |
|
642 (* k is index of current start component. *) |
|
643 |
|
644 fun processComponent (k, comp) = |
|
645 let |
|
646 (* all edges pointing away from the component *) |
|
647 (* (Term.term * less) list *) |
|
648 val allEdges = flat (map (adjacent_term g) comp); |
|
649 |
|
650 (* choose those edges pointing to nodes outside |
|
651 the current component *) |
|
652 |
|
653 fun selectEdges [] = [] |
|
654 | selectEdges ((v,l)::es) = let val k' = getIndex v ntc in |
|
655 if k' = k then selectEdges es else (k', l) :: (selectEdges es) end; |
|
656 |
|
657 (* Insert edge into sorted list of edges, where edge is |
|
658 only added if |
|
659 - it is found for the first time |
|
660 - it is a <= edge and no parallel < edge was found earlier |
|
661 - it is a < edge |
|
662 *) |
|
663 |
|
664 fun insert (h,l) [] = [(h,l)] |
|
665 | insert (h,l) ((k',l')::es) = if h = k' then ( |
|
666 case l of (Less (_, _, _)) => (h,l)::es |
|
667 | _ => (case l' of (Less (_, _, _)) => (h,l')::es |
|
668 | _ => (k',l)::es) ) |
|
669 else (k',l'):: insert (h,l) es; |
|
670 |
|
671 (* Reorganise list of edges such that |
|
672 - duplicate edges are removed |
|
673 - if a < edge and a <= edge exist at the same time, |
|
674 remove <= edge *) |
|
675 |
|
676 fun sortEdges [] sorted = sorted: (int * less) list |
|
677 | sortEdges (e::es) sorted = sortEdges es (insert e sorted); |
|
678 |
|
679 in |
|
680 (k, (sortEdges (selectEdges allEdges) [])) |
|
681 end; |
|
682 |
|
683 |
|
684 in map processComponent IndexComp end; |
|
685 |
|
686 (* Remove ``less'' edge info from graph *) |
|
687 (* type ('a * ('a * less) list) list *) |
|
688 fun stripOffLess g = map (fn (v, desc) => (v,map (fn (u,l) => u) desc)) g; |
|
689 |
|
690 |
|
691 |
|
692 (* *********************************************************************** *) |
|
693 (* *) |
|
694 (* dfs_term g u v: *) |
|
695 (* (Term.term *(Term.term * less) list) list -> *) |
|
696 (* Term.term -> Term.term -> (bool * less list) *) |
|
697 (* *) |
|
698 (* Depth first search of v from u. *) |
|
699 (* Returns (true, path(u, v)) if successful, otherwise (false, []). *) |
|
700 (* *) |
|
701 (* *********************************************************************** *) |
|
702 |
|
703 |
|
704 fun dfs_term g u v = |
|
705 let |
|
706 (* TODO: this comment is unclear *) |
|
707 (* Liste der gegangenen Kanten, |
|
708 die Kante e die zum Vorgaenger eines Knoten u gehoert ist jene |
|
709 für die gilt (upper e) = u *) |
|
710 val pred : less list ref = ref nil; |
|
711 val visited: term list ref = ref nil; |
|
712 |
|
713 fun been_visited v = exists (fn w => w aconv v) (!visited) |
|
714 |
|
715 fun dfs_visit u' = |
|
716 let val _ = visited := u' :: (!visited) |
|
717 |
|
718 fun update l = let val _ = pred := l ::(!pred) in () end; |
|
719 |
|
720 in if been_visited v then () |
|
721 else (app (fn (v',l) => if been_visited v' then () else ( |
|
722 update l; |
|
723 dfs_visit v'; ()) )) (adjacent_term g u') |
|
724 end |
|
725 |
|
726 in |
|
727 dfs_visit u; |
|
728 if (been_visited v) then (true, (!pred)) else (false , []) |
|
729 end; |
|
730 |
|
731 |
|
732 (* *********************************************************************** *) |
|
733 (* *) |
|
734 (* completeTermPath u v g: *) |
|
735 (* Term.term -> Term.term -> (Term.term * (Term.term * less) list) list *) |
|
736 (* -> less list *) |
|
737 (* *) |
|
738 (* Complete the path from u to v in graph g. Path search is performed *) |
|
739 (* with dfs_term g u v. This yields for each node v' its predecessor u' *) |
|
740 (* and the edge u' -> v'. Allows traversing graph backwards from v and *) |
|
741 (* finding the path u -> v. *) |
|
742 (* *) |
|
743 (* *********************************************************************** *) |
|
744 |
|
745 |
|
746 fun completeTermPath u v g = |
|
747 let |
|
748 |
|
749 val (found, pred) = dfs_term g u v; |
|
750 |
|
751 fun path x y = |
|
752 let |
|
753 |
|
754 (* find predecessor u of node v and the edge u -> v *) |
|
755 |
|
756 fun lookup v [] = raise Cannot |
|
757 | lookup v (e::es) = if (upper e) aconv v then e else lookup v es; |
|
758 |
|
759 (* traverse path backwards and return list of visited edges *) |
|
760 fun rev_path v = |
|
761 let val l = lookup v pred |
|
762 val u = lower l; |
|
763 in |
|
764 if u aconv x then [l] |
|
765 else (rev_path u) @ [l] |
|
766 end |
|
767 in rev_path y end; |
|
768 |
|
769 in |
|
770 if found then (if u aconv v then [(Le (u, v, (Thm ([], Less.le_refl))))] |
|
771 else path u v ) else raise Cannot |
|
772 end; |
|
773 |
|
774 |
|
775 (* *********************************************************************** *) |
|
776 (* *) |
|
777 (* dfs_int g u v: *) |
|
778 (* (int *(int * less) list) list -> int -> int *) |
|
779 (* -> (bool *(int* less) list) *) |
|
780 (* *) |
|
781 (* Depth first search of v from u. *) |
|
782 (* Returns (true, path(u, v)) if successful, otherwise (false, []). *) |
|
783 (* *) |
|
784 (* *********************************************************************** *) |
|
785 |
|
786 fun dfs_int g u v = |
|
787 let |
|
788 val pred : (int * less ) list ref = ref nil; |
|
789 val visited: int list ref = ref nil; |
|
790 |
|
791 fun been_visited v = exists (fn w => w = v) (!visited) |
|
792 |
|
793 fun dfs_visit u' = |
|
794 let val _ = visited := u' :: (!visited) |
|
795 |
|
796 fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end; |
|
797 |
|
798 in if been_visited v then () |
|
799 else (app (fn (v',l) => if been_visited v' then () else ( |
|
800 update (v',l); |
|
801 dfs_visit v'; ()) )) (adjacent g u') |
|
802 |
|
803 end |
|
804 |
|
805 in |
|
806 dfs_visit u; |
|
807 if (been_visited v) then (true, (!pred)) else (false , []) |
|
808 end; |
|
809 |
|
810 |
|
811 (* *********************************************************************** *) |
|
812 (* *) |
|
813 (* findProof (g2, cg2, neqEdges, components, ntc) subgoal: *) |
|
814 (* (Term.term * (Term.term * less) list) list * *) |
|
815 (* (int * (int * less) list) list * less list * Term.term list list *) |
|
816 (* * ( (Term.term * int) -> proof *) |
|
817 (* *) |
|
818 (* findProof constructs from graphs (g2, cg2) and neqEdges a proof for *) |
|
819 (* subgoal. Raises exception Cannot if this is not possible. *) |
|
820 (* *) |
|
821 (* *********************************************************************** *) |
|
822 |
|
823 fun findProof (g2, cg2, neqEdges, components, ntc ) subgoal = |
|
824 let |
|
825 |
|
826 (* complete path x y from component graph *) |
|
827 fun completeComponentPath x y predlist = |
|
828 let |
|
829 val xi = getIndex x ntc |
|
830 val yi = getIndex y ntc |
|
831 |
|
832 fun lookup k [] = raise Cannot |
|
833 | lookup k ((h,l)::us) = if k = h then l else lookup k us; |
|
834 |
|
835 fun rev_completeComponentPath y' = |
|
836 let val edge = lookup (getIndex y' ntc) predlist |
|
837 val u = lower edge |
|
838 val v = upper edge |
|
839 in |
|
840 if (getIndex u ntc) = xi then |
|
841 (completeTermPath x u g2)@[edge]@(completeTermPath v y' g2) |
|
842 else (rev_completeComponentPath u)@[edge]@(completeTermPath v y' g2) |
|
843 end |
|
844 in |
|
845 if x aconv y then |
|
846 [(Le (x, y, (Thm ([], Less.le_refl))))] |
|
847 else ( if xi = yi then completeTermPath x y g2 |
|
848 else rev_completeComponentPath y ) |
|
849 end; |
|
850 |
|
851 (* ******************************************************************* *) |
|
852 (* findLess e x y xi yi xreachable yreachable *) |
|
853 (* *) |
|
854 (* Find a path from x through e to y, of weight < *) |
|
855 (* ******************************************************************* *) |
|
856 |
|
857 fun findLess e x y xi yi Xreachable Yreachable = |
|
858 let val u = lower e |
|
859 val v = upper e |
|
860 val ui = getIndex u ntc |
|
861 val vi = getIndex v ntc |
|
862 |
|
863 in |
|
864 if ui mem Xreachable andalso vi mem Xreachable andalso |
|
865 ui mem Yreachable andalso vi mem Yreachable then ( |
|
866 |
|
867 (case e of (Less (_, _, _)) => |
|
868 let |
|
869 val (xufound, xupred) = dfs_int cg2 xi (getIndex u ntc) |
|
870 in |
|
871 if xufound then ( |
|
872 let |
|
873 val (vyfound, vypred) = dfs_int cg2 (getIndex v ntc) yi |
|
874 in |
|
875 if vyfound then ( |
|
876 let |
|
877 val xypath = (completeComponentPath x u xupred)@[e]@(completeComponentPath v y vypred) |
|
878 val xyLesss = transPath (tl xypath, hd xypath) |
|
879 in |
|
880 if xyLesss subsumes subgoal then Some (getprf xyLesss) |
|
881 else None |
|
882 end) |
|
883 else None |
|
884 end) |
|
885 else None |
|
886 end |
|
887 | _ => |
|
888 let val (xufound, xupred) = dfs_int cg2 xi (getIndex u ntc) |
|
889 in |
|
890 if xufound then ( |
|
891 let |
|
892 val (uvfound, uvpred) = dfs_int cg2 (getIndex u ntc) (getIndex v ntc) |
|
893 in |
|
894 if uvfound then ( |
|
895 let |
|
896 val (vyfound, vypred) = dfs_int cg2 (getIndex v ntc) yi |
|
897 in |
|
898 if vyfound then ( |
|
899 let |
|
900 val uvpath = completeComponentPath u v uvpred |
|
901 val uvLesss = mergeLess ( transPath (tl uvpath, hd uvpath), e) |
|
902 val xypath = (completeComponentPath x u xupred)@[uvLesss]@(completeComponentPath v y vypred) |
|
903 val xyLesss = transPath (tl xypath, hd xypath) |
|
904 in |
|
905 if xyLesss subsumes subgoal then Some (getprf xyLesss) |
|
906 else None |
|
907 end ) |
|
908 else None |
|
909 end) |
|
910 else None |
|
911 end ) |
|
912 else None |
|
913 end ) |
|
914 ) else None |
|
915 end; |
|
916 |
|
917 |
|
918 in |
|
919 (* looking for x <= y: any path from x to y is sufficient *) |
|
920 case subgoal of (Le (x, y, _)) => ( |
|
921 |
|
922 let |
|
923 val xi = getIndex x ntc |
|
924 val yi = getIndex y ntc |
|
925 (* sucht im Komponentengraphen einen Weg von der Komponente in der x liegt |
|
926 zu der in der y liegt *) |
|
927 val (found, pred) = dfs_int cg2 xi yi |
|
928 in |
|
929 if found then ( |
|
930 let val xypath = completeComponentPath x y pred |
|
931 val xyLesss = transPath (tl xypath, hd xypath) |
|
932 in |
|
933 (case xyLesss of |
|
934 (Less (_, _, q)) => if xyLesss subsumes subgoal then (Thm ([q], Less.less_imp_le)) |
|
935 else raise Cannot |
|
936 | _ => if xyLesss subsumes subgoal then (getprf xyLesss) |
|
937 else raise Cannot) |
|
938 end ) |
|
939 else raise Cannot |
|
940 end |
|
941 |
|
942 ) |
|
943 (* looking for x < y: particular path required, which is not necessarily |
|
944 found by normal dfs *) |
|
945 | (Less (x, y, _)) => ( |
|
946 let |
|
947 val xi = getIndex x ntc |
|
948 val yi = getIndex y ntc |
|
949 val cg2' = stripOffLess cg2 |
|
950 val cg2'_transpose = transpose cg2' |
|
951 (* alle von x aus erreichbaren Komponenten *) |
|
952 val xreachable = dfs_int_reachable cg2' xi |
|
953 (* all comonents reachable from y in the transposed graph cg2' *) |
|
954 val yreachable = dfs_int_reachable cg2'_transpose yi |
|
955 (* for all edges u ~= v or u < v check if they are part of path x < y *) |
|
956 fun processNeqEdges [] = raise Cannot |
|
957 | processNeqEdges (e::es) = |
|
958 case (findLess e x y xi yi xreachable yreachable) of (Some prf) => prf |
|
959 | _ => processNeqEdges es |
|
960 |
|
961 in |
|
962 processNeqEdges neqEdges |
|
963 end |
|
964 |
|
965 ) |
|
966 | (NotEq (x, y, _)) => ( |
|
967 |
|
968 let val xi = getIndex x ntc |
|
969 val yi = getIndex y ntc |
|
970 val cg2' = stripOffLess cg2 |
|
971 val cg2'_transpose = transpose cg2' |
|
972 val xreachable = dfs_int_reachable cg2' xi |
|
973 val yreachable = dfs_int_reachable cg2'_transpose yi |
|
974 |
|
975 fun processNeqEdges [] = raise Cannot |
|
976 | processNeqEdges (e::es) = ( |
|
977 let val u = lower e |
|
978 val v = upper e |
|
979 val ui = getIndex u ntc |
|
980 val vi = getIndex v ntc |
|
981 |
|
982 in |
|
983 (* if x ~= y follows from edge e *) |
|
984 if e subsumes subgoal then ( |
|
985 case e of (Less (u, v, q)) => ( |
|
986 if u aconv x andalso v aconv y then (Thm ([q], Less.less_imp_neq)) |
|
987 else (Thm ([(Thm ([q], Less.less_imp_neq))], thm "not_sym")) |
|
988 ) |
|
989 | (NotEq (u,v, q)) => ( |
|
990 if u aconv x andalso v aconv y then q |
|
991 else (Thm ([q], thm "not_sym")) |
|
992 ) |
|
993 ) |
|
994 (* if SCC_x is linked to SCC_y via edge e *) |
|
995 else if ui = xi andalso vi = yi then ( |
|
996 case e of (Less (_, _,_)) => ( |
|
997 let val xypath = (completeTermPath x u g2) @ [e] @ (completeTermPath v y g2) |
|
998 val xyLesss = transPath (tl xypath, hd xypath) |
|
999 in (Thm ([getprf xyLesss], Less.less_imp_neq)) end) |
|
1000 | _ => ( |
|
1001 let val xupath = completeTermPath x u g2 |
|
1002 val uxpath = completeTermPath u x g2 |
|
1003 val vypath = completeTermPath v y g2 |
|
1004 val yvpath = completeTermPath y v g2 |
|
1005 val xuLesss = transPath (tl xupath, hd xupath) |
|
1006 val uxLesss = transPath (tl uxpath, hd uxpath) |
|
1007 val vyLesss = transPath (tl vypath, hd vypath) |
|
1008 val yvLesss = transPath (tl yvpath, hd yvpath) |
|
1009 val x_eq_u = (Thm ([(getprf xuLesss),(getprf uxLesss)], Less.eqI)) |
|
1010 val v_eq_y = (Thm ([(getprf vyLesss),(getprf yvLesss)], Less.eqI)) |
|
1011 in |
|
1012 (Thm ([x_eq_u , (getprf e), v_eq_y ], Less.eq_neq_eq_imp_neq)) |
|
1013 end |
|
1014 ) |
|
1015 ) else if ui = yi andalso vi = xi then ( |
|
1016 case e of (Less (_, _,_)) => ( |
|
1017 let val xypath = (completeTermPath y u g2) @ [e] @ (completeTermPath v x g2) |
|
1018 val xyLesss = transPath (tl xypath, hd xypath) |
|
1019 in (Thm ([(Thm ([getprf xyLesss], Less.less_imp_neq))] , thm "not_sym")) end ) |
|
1020 | _ => ( |
|
1021 |
|
1022 let val yupath = completeTermPath y u g2 |
|
1023 val uypath = completeTermPath u y g2 |
|
1024 val vxpath = completeTermPath v x g2 |
|
1025 val xvpath = completeTermPath x v g2 |
|
1026 val yuLesss = transPath (tl yupath, hd yupath) |
|
1027 val uyLesss = transPath (tl uypath, hd uypath) |
|
1028 val vxLesss = transPath (tl vxpath, hd vxpath) |
|
1029 val xvLesss = transPath (tl xvpath, hd xvpath) |
|
1030 val y_eq_u = (Thm ([(getprf yuLesss),(getprf uyLesss)], Less.eqI)) |
|
1031 val v_eq_x = (Thm ([(getprf vxLesss),(getprf xvLesss)], Less.eqI)) |
|
1032 in |
|
1033 (Thm ([(Thm ([y_eq_u , (getprf e), v_eq_x ], Less.eq_neq_eq_imp_neq))], thm "not_sym")) |
|
1034 end |
|
1035 ) |
|
1036 ) else ( |
|
1037 (* there exists a path x < y or y < x such that |
|
1038 x ~= y may be concluded *) |
|
1039 case (findLess e x y xi yi xreachable yreachable) of |
|
1040 (Some prf) => (Thm ([prf], Less.less_imp_neq)) |
|
1041 | None => ( |
|
1042 let |
|
1043 val yr = dfs_int_reachable cg2' yi |
|
1044 val xr = dfs_int_reachable cg2'_transpose xi |
|
1045 in |
|
1046 case (findLess e y x yi xi yr xr) of |
|
1047 (Some prf) => (Thm ([(Thm ([prf], Less.less_imp_neq))], thm "not_sym")) |
|
1048 | _ => processNeqEdges es |
|
1049 end) |
|
1050 ) end) |
|
1051 in processNeqEdges neqEdges end |
|
1052 ) |
|
1053 end; |
|
1054 |
|
1055 |
|
1056 (* *********************************************************************** *) |
|
1057 (* *) |
|
1058 (* checkComponents g components ntc neqEdges: *) |
|
1059 (* (Term.term * (Term.term * less) list) list -> Term.term list list -> *) |
|
1060 (* (Term.term * int) -> less list -> bool *) |
|
1061 (* *) |
|
1062 (* For each edge in the list neqEdges check if it leads to a contradiction.*) |
|
1063 (* We have a contradiction for edge u ~= v and u < v if: *) |
|
1064 (* - u and v are in the same component, *) |
|
1065 (* that is, a path u <= v and a path v <= u exist, hence u = v. *) |
|
1066 (* From irreflexivity of < follows u < u or v < v. Ex false quodlibet. *) |
|
1067 (* *) |
|
1068 (* *) |
|
1069 (* *********************************************************************** *) |
|
1070 |
|
1071 |
|
1072 fun checkComponents g components ntc neqEdges = |
|
1073 let |
|
1074 (* Construct proof by contradiction for edge *) |
|
1075 fun handleContr edge = |
|
1076 (case edge of |
|
1077 (Less (x, y, _)) => ( |
|
1078 let |
|
1079 val xxpath = edge :: (completeTermPath y x g) |
|
1080 val xxLesss = transPath (tl xxpath, hd xxpath) |
|
1081 val q = getprf xxLesss |
|
1082 in |
|
1083 raise (Contr (Thm ([q], Less.less_reflE ))) |
|
1084 end |
|
1085 ) |
|
1086 | (NotEq (x, y, _)) => ( |
|
1087 let |
|
1088 val xypath = (completeTermPath x y g) |
|
1089 val yxpath = (completeTermPath y x g) |
|
1090 val xyLesss = transPath (tl xypath, hd xypath) |
|
1091 val yxLesss = transPath (tl yxpath, hd yxpath) |
|
1092 val q = getprf (mergeLess ((mergeLess (edge, xyLesss)),yxLesss )) |
|
1093 in |
|
1094 raise (Contr (Thm ([q], Less.less_reflE ))) |
|
1095 end |
|
1096 ) |
|
1097 | _ => error "trans_tac/checkCompoents/handleContr: invalid Contradiction"); |
|
1098 |
|
1099 (* Check each edge in neqEdges for contradiction. |
|
1100 If there is a contradiction, call handleContr, otherwise do nothing. *) |
|
1101 fun checkNeqEdges [] = () |
|
1102 | checkNeqEdges (e::es) = |
|
1103 (case e of (Less (u, v, _)) => |
|
1104 if (getIndex u ntc) = (getIndex v ntc) then handleContr e g |
|
1105 else checkNeqEdges es |
|
1106 | (NotEq (u, v, _)) => |
|
1107 if (getIndex u ntc) = (getIndex v ntc) then handleContr e g |
|
1108 else checkNeqEdges es |
|
1109 | _ => checkNeqEdges es) |
|
1110 |
|
1111 in if g = [] then () else checkNeqEdges neqEdges end; |
|
1112 |
|
1113 (* *********************************************************************** *) |
|
1114 (* *) |
|
1115 (* solvePartialOrder sign (asms,concl) : *) |
|
1116 (* Sign.sg -> less list * Term.term -> proof list *) |
|
1117 (* *) |
|
1118 (* Find proof if possible for partial orders. *) |
|
1119 (* *) |
|
1120 (* *********************************************************************** *) |
|
1121 |
|
1122 fun solvePartialOrder sign (asms, concl) = |
|
1123 let |
|
1124 val (g1, g2, neqEdges) = buildGraphs (asms, [], [],[]) |
|
1125 val components = scc_term g1 |
|
1126 val ntc = indexNodes (indexComps components) |
|
1127 val cg2 = evalcompgraph components g2 ntc |
|
1128 in |
|
1129 (* Check for contradiction within assumptions *) |
|
1130 checkComponents g2 components ntc neqEdges; |
|
1131 let |
|
1132 val (subgoals, prf) = mkconcl_partial sign concl |
|
1133 fun solve facts less = |
|
1134 (case triv_solv less of None => findProof (g2, cg2, neqEdges, components, ntc) less |
|
1135 | Some prf => prf ) |
|
1136 in |
|
1137 map (solve asms) subgoals |
|
1138 end |
|
1139 end; |
|
1140 |
|
1141 (* *********************************************************************** *) |
|
1142 (* *) |
|
1143 (* solveTotalOrder sign (asms,concl) : *) |
|
1144 (* Sign.sg -> less list * Term.term -> proof list *) |
|
1145 (* *) |
|
1146 (* Find proof if possible for linear orders. *) |
|
1147 (* *) |
|
1148 (* *********************************************************************** *) |
|
1149 |
|
1150 fun solveTotalOrder sign (asms, concl) = |
|
1151 let |
|
1152 val (g1, g2, neqEdges) = buildGraphs (asms, [], [],[]) |
|
1153 val components = scc_term g1 |
|
1154 val ntc = indexNodes (indexComps components) |
|
1155 val cg2 = evalcompgraph components g2 ntc |
|
1156 in |
|
1157 checkComponents g2 components ntc neqEdges; |
|
1158 let |
|
1159 val (subgoals, prf) = mkconcl_linear sign concl |
|
1160 fun solve facts less = |
|
1161 (case triv_solv less of None => findProof (g2, cg2, neqEdges, components, ntc) less |
|
1162 | Some prf => prf ) |
|
1163 in |
|
1164 map (solve asms) subgoals |
|
1165 end |
|
1166 end; |
|
1167 |
|
1168 |
|
1169 (* partial_tac - solves linear/total orders *) |
|
1170 |
|
1171 val partial_tac = SUBGOAL (fn (A, n, sign) => |
|
1172 let |
|
1173 val rfrees = map Free (rename_wrt_term A (Logic.strip_params A)) |
|
1174 val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A) |
|
1175 val C = subst_bounds (rfrees, Logic.strip_assums_concl A) |
|
1176 val lesss = flat (ListPair.map (mkasm_partial sign) (Hs, 0 upto (length Hs - 1))) |
|
1177 val prfs = solvePartialOrder sign (lesss, C); |
|
1178 val (subgoals, prf) = mkconcl_partial sign C; |
|
1179 in |
|
1180 METAHYPS (fn asms => |
|
1181 let val thms = map (prove asms) prfs |
|
1182 in rtac (prove thms prf) 1 end) n |
|
1183 end |
|
1184 handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n |
|
1185 | Cannot => no_tac |
|
1186 ); |
|
1187 |
|
1188 (* linear_tac - solves linear/total orders *) |
|
1189 |
|
1190 val linear_tac = SUBGOAL (fn (A, n, sign) => |
|
1191 let |
|
1192 val rfrees = map Free (rename_wrt_term A (Logic.strip_params A)) |
|
1193 val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A) |
|
1194 val C = subst_bounds (rfrees, Logic.strip_assums_concl A) |
|
1195 val lesss = flat (ListPair.map (mkasm_linear sign) (Hs, 0 upto (length Hs - 1))) |
|
1196 val prfs = solveTotalOrder sign (lesss, C); |
|
1197 val (subgoals, prf) = mkconcl_linear sign C; |
|
1198 in |
|
1199 METAHYPS (fn asms => |
|
1200 let val thms = map (prove asms) prfs |
|
1201 in rtac (prove thms prf) 1 end) n |
|
1202 end |
|
1203 handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n |
|
1204 | Cannot => no_tac); |
|
1205 |
|
1206 end; |
|
1207 |