|
1 (* Title: src/Provers/preorder.ML |
|
2 Author: Oliver Kutter, TU Muenchen |
|
3 |
|
4 Reasoner for simple transitivity and quasi orders. |
|
5 *) |
|
6 |
|
7 (* |
|
8 |
|
9 The package provides tactics trans_tac and quasi_tac that use |
|
10 premises of the form |
|
11 |
|
12 t = u, t ~= u, t < u and t <= u |
|
13 |
|
14 to |
|
15 - either derive a contradiction, in which case the conclusion can be |
|
16 any term, |
|
17 - or prove the concluson, which must be of the form t ~= u, t < u or |
|
18 t <= u. |
|
19 |
|
20 Details: |
|
21 |
|
22 1. trans_tac: |
|
23 Only premises of form t <= u are used and the conclusion must be of |
|
24 the same form. The conclusion is proved, if possible, by a chain of |
|
25 transitivity from the assumptions. |
|
26 |
|
27 2. quasi_tac: |
|
28 <= is assumed to be a quasi order and < its strict relative, defined |
|
29 as t < u == t <= u & t ~= u. Again, the conclusion is proved from |
|
30 the assumptions. |
|
31 Note that the presence of a strict relation is not necessary for |
|
32 quasi_tac. Configure decomp_quasi to ignore < and ~=. A list of |
|
33 required theorems for both situations is given below. |
|
34 *) |
|
35 |
|
36 signature LESS_ARITH = |
|
37 sig |
|
38 (* Transitivity of <= |
|
39 Note that transitivities for < hold for partial orders only. *) |
|
40 val le_trans: thm (* [| x <= y; y <= z |] ==> x <= z *) |
|
41 |
|
42 (* Additional theorem for quasi orders *) |
|
43 val le_refl: thm (* x <= x *) |
|
44 val eqD1: thm (* x = y ==> x <= y *) |
|
45 val eqD2: thm (* x = y ==> y <= x *) |
|
46 |
|
47 (* Additional theorems for premises of the form x < y *) |
|
48 val less_reflE: thm (* x < x ==> P *) |
|
49 val less_imp_le : thm (* x < y ==> x <= y *) |
|
50 |
|
51 (* Additional theorems for premises of the form x ~= y *) |
|
52 val le_neq_trans : thm (* [| x <= y ; x ~= y |] ==> x < y *) |
|
53 val neq_le_trans : thm (* [| x ~= y ; x <= y |] ==> x < y *) |
|
54 |
|
55 (* Additional theorem for goals of form x ~= y *) |
|
56 val less_imp_neq : thm (* x < y ==> x ~= y *) |
|
57 |
|
58 (* Analysis of premises and conclusion *) |
|
59 (* decomp_x (`x Rel y') should yield SOME (x, Rel, y) |
|
60 where Rel is one of "<", "<=", "=" and "~=", |
|
61 other relation symbols cause an error message *) |
|
62 (* decomp_trans is used by trans_tac, it may only return Rel = "<=" *) |
|
63 val decomp_trans: theory -> term -> (term * string * term) option |
|
64 (* decomp_quasi is used by quasi_tac *) |
|
65 val decomp_quasi: theory -> term -> (term * string * term) option |
|
66 end; |
|
67 |
|
68 signature QUASI_TAC = |
|
69 sig |
|
70 val trans_tac: Proof.context -> int -> tactic |
|
71 val quasi_tac: Proof.context -> int -> tactic |
|
72 end; |
|
73 |
|
74 functor Quasi_Tac(Less: LESS_ARITH): QUASI_TAC = |
|
75 struct |
|
76 |
|
77 (* Internal datatype for the proof *) |
|
78 datatype proof |
|
79 = Asm of int |
|
80 | Thm of proof list * thm; |
|
81 |
|
82 exception Cannot; |
|
83 (* Internal exception, raised if conclusion cannot be derived from |
|
84 assumptions. *) |
|
85 exception Contr of proof; |
|
86 (* Internal exception, raised if contradiction ( x < x ) was derived *) |
|
87 |
|
88 fun prove asms = |
|
89 let |
|
90 fun pr (Asm i) = nth asms i |
|
91 | pr (Thm (prfs, thm)) = map pr prfs MRS thm; |
|
92 in pr end; |
|
93 |
|
94 (* Internal datatype for inequalities *) |
|
95 datatype less |
|
96 = Less of term * term * proof |
|
97 | Le of term * term * proof |
|
98 | NotEq of term * term * proof; |
|
99 |
|
100 (* Misc functions for datatype less *) |
|
101 fun lower (Less (x, _, _)) = x |
|
102 | lower (Le (x, _, _)) = x |
|
103 | lower (NotEq (x,_,_)) = x; |
|
104 |
|
105 fun upper (Less (_, y, _)) = y |
|
106 | upper (Le (_, y, _)) = y |
|
107 | upper (NotEq (_,y,_)) = y; |
|
108 |
|
109 fun getprf (Less (_, _, p)) = p |
|
110 | getprf (Le (_, _, p)) = p |
|
111 | getprf (NotEq (_,_, p)) = p; |
|
112 |
|
113 (* ************************************************************************ *) |
|
114 (* *) |
|
115 (* mkasm_trans sign (t, n) : theory -> (Term.term * int) -> less *) |
|
116 (* *) |
|
117 (* Tuple (t, n) (t an assumption, n its index in the assumptions) is *) |
|
118 (* translated to an element of type less. *) |
|
119 (* Only assumptions of form x <= y are used, all others are ignored *) |
|
120 (* *) |
|
121 (* ************************************************************************ *) |
|
122 |
|
123 fun mkasm_trans thy (t, n) = |
|
124 case Less.decomp_trans thy t of |
|
125 SOME (x, rel, y) => |
|
126 (case rel of |
|
127 "<=" => [Le (x, y, Asm n)] |
|
128 | _ => error ("trans_tac: unknown relation symbol ``" ^ rel ^ |
|
129 "''returned by decomp_trans.")) |
|
130 | NONE => []; |
|
131 |
|
132 (* ************************************************************************ *) |
|
133 (* *) |
|
134 (* mkasm_quasi sign (t, n) : theory -> (Term.term * int) -> less *) |
|
135 (* *) |
|
136 (* Tuple (t, n) (t an assumption, n its index in the assumptions) is *) |
|
137 (* translated to an element of type less. *) |
|
138 (* Quasi orders only. *) |
|
139 (* *) |
|
140 (* ************************************************************************ *) |
|
141 |
|
142 fun mkasm_quasi thy (t, n) = |
|
143 case Less.decomp_quasi thy t of |
|
144 SOME (x, rel, y) => (case rel of |
|
145 "<" => if (x aconv y) then raise Contr (Thm ([Asm n], Less.less_reflE)) |
|
146 else [Less (x, y, Asm n)] |
|
147 | "<=" => [Le (x, y, Asm n)] |
|
148 | "=" => [Le (x, y, Thm ([Asm n], Less.eqD1)), |
|
149 Le (y, x, Thm ([Asm n], Less.eqD2))] |
|
150 | "~=" => if (x aconv y) then |
|
151 raise Contr (Thm ([(Thm ([(Thm ([], Less.le_refl)) ,(Asm n)], Less.le_neq_trans))], Less.less_reflE)) |
|
152 else [ NotEq (x, y, Asm n), |
|
153 NotEq (y, x,Thm ( [Asm n], @{thm not_sym}))] |
|
154 | _ => error ("quasi_tac: unknown relation symbol ``" ^ rel ^ |
|
155 "''returned by decomp_quasi.")) |
|
156 | NONE => []; |
|
157 |
|
158 |
|
159 (* ************************************************************************ *) |
|
160 (* *) |
|
161 (* mkconcl_trans sign t : theory -> Term.term -> less *) |
|
162 (* *) |
|
163 (* Translates conclusion t to an element of type less. *) |
|
164 (* Only for Conclusions of form x <= y or x < y. *) |
|
165 (* *) |
|
166 (* ************************************************************************ *) |
|
167 |
|
168 |
|
169 fun mkconcl_trans thy t = |
|
170 case Less.decomp_trans thy t of |
|
171 SOME (x, rel, y) => (case rel of |
|
172 "<=" => (Le (x, y, Asm ~1), Asm 0) |
|
173 | _ => raise Cannot) |
|
174 | NONE => raise Cannot; |
|
175 |
|
176 |
|
177 (* ************************************************************************ *) |
|
178 (* *) |
|
179 (* mkconcl_quasi sign t : theory -> Term.term -> less *) |
|
180 (* *) |
|
181 (* Translates conclusion t to an element of type less. *) |
|
182 (* Quasi orders only. *) |
|
183 (* *) |
|
184 (* ************************************************************************ *) |
|
185 |
|
186 fun mkconcl_quasi thy t = |
|
187 case Less.decomp_quasi thy t of |
|
188 SOME (x, rel, y) => (case rel of |
|
189 "<" => ([Less (x, y, Asm ~1)], Asm 0) |
|
190 | "<=" => ([Le (x, y, Asm ~1)], Asm 0) |
|
191 | "~=" => ([NotEq (x,y, Asm ~1)], Asm 0) |
|
192 | _ => raise Cannot) |
|
193 | NONE => raise Cannot; |
|
194 |
|
195 |
|
196 (* ******************************************************************* *) |
|
197 (* *) |
|
198 (* mergeLess (less1,less2): less * less -> less *) |
|
199 (* *) |
|
200 (* Merge to elements of type less according to the following rules *) |
|
201 (* *) |
|
202 (* x <= y && y <= z ==> x <= z *) |
|
203 (* x <= y && x ~= y ==> x < y *) |
|
204 (* x ~= y && x <= y ==> x < y *) |
|
205 (* *) |
|
206 (* ******************************************************************* *) |
|
207 |
|
208 fun mergeLess (Le (x, _, p) , Le (_ , z, q)) = |
|
209 Le (x, z, Thm ([p,q] , Less.le_trans)) |
|
210 | mergeLess (Le (x, z, p) , NotEq (x', z', q)) = |
|
211 if (x aconv x' andalso z aconv z' ) |
|
212 then Less (x, z, Thm ([p,q] , Less.le_neq_trans)) |
|
213 else error "quasi_tac: internal error le_neq_trans" |
|
214 | mergeLess (NotEq (x, z, p) , Le (x' , z', q)) = |
|
215 if (x aconv x' andalso z aconv z') |
|
216 then Less (x, z, Thm ([p,q] , Less.neq_le_trans)) |
|
217 else error "quasi_tac: internal error neq_le_trans" |
|
218 | mergeLess (_, _) = |
|
219 error "quasi_tac: internal error: undefined case"; |
|
220 |
|
221 |
|
222 (* ******************************************************************** *) |
|
223 (* tr checks for valid transitivity step *) |
|
224 (* ******************************************************************** *) |
|
225 |
|
226 infix tr; |
|
227 fun (Le (_, y, _)) tr (Le (x', _, _)) = ( y aconv x' ) |
|
228 | _ tr _ = false; |
|
229 |
|
230 (* ******************************************************************* *) |
|
231 (* *) |
|
232 (* transPath (Lesslist, Less): (less list * less) -> less *) |
|
233 (* *) |
|
234 (* If a path represented by a list of elements of type less is found, *) |
|
235 (* this needs to be contracted to a single element of type less. *) |
|
236 (* Prior to each transitivity step it is checked whether the step is *) |
|
237 (* valid. *) |
|
238 (* *) |
|
239 (* ******************************************************************* *) |
|
240 |
|
241 fun transPath ([],lesss) = lesss |
|
242 | transPath (x::xs,lesss) = |
|
243 if lesss tr x then transPath (xs, mergeLess(lesss,x)) |
|
244 else error "trans/quasi_tac: internal error transpath"; |
|
245 |
|
246 (* ******************************************************************* *) |
|
247 (* *) |
|
248 (* less1 subsumes less2 : less -> less -> bool *) |
|
249 (* *) |
|
250 (* subsumes checks whether less1 implies less2 *) |
|
251 (* *) |
|
252 (* ******************************************************************* *) |
|
253 |
|
254 infix subsumes; |
|
255 fun (Le (x, y, _)) subsumes (Le (x', y', _)) = |
|
256 (x aconv x' andalso y aconv y') |
|
257 | (Le _) subsumes (Less _) = |
|
258 error "trans/quasi_tac: internal error: Le cannot subsume Less" |
|
259 | (NotEq(x,y,_)) subsumes (NotEq(x',y',_)) = x aconv x' andalso y aconv y' orelse x aconv y' andalso y aconv x' |
|
260 | _ subsumes _ = false; |
|
261 |
|
262 (* ******************************************************************* *) |
|
263 (* *) |
|
264 (* triv_solv less1 : less -> proof option *) |
|
265 (* *) |
|
266 (* Solves trivial goal x <= x. *) |
|
267 (* *) |
|
268 (* ******************************************************************* *) |
|
269 |
|
270 fun triv_solv (Le (x, x', _)) = |
|
271 if x aconv x' then SOME (Thm ([], Less.le_refl)) |
|
272 else NONE |
|
273 | triv_solv _ = NONE; |
|
274 |
|
275 (* ********************************************************************* *) |
|
276 (* Graph functions *) |
|
277 (* ********************************************************************* *) |
|
278 |
|
279 (* *********************************************************** *) |
|
280 (* Functions for constructing graphs *) |
|
281 (* *********************************************************** *) |
|
282 |
|
283 fun addEdge (v,d,[]) = [(v,d)] |
|
284 | addEdge (v,d,((u,dl)::el)) = if v aconv u then ((v,d@dl)::el) |
|
285 else (u,dl):: (addEdge(v,d,el)); |
|
286 |
|
287 (* ********************************************************************** *) |
|
288 (* *) |
|
289 (* mkQuasiGraph constructs from a list of objects of type less a graph g, *) |
|
290 (* by taking all edges that are candidate for a <=, and a list neqE, by *) |
|
291 (* taking all edges that are candiate for a ~= *) |
|
292 (* *) |
|
293 (* ********************************************************************** *) |
|
294 |
|
295 fun mkQuasiGraph [] = ([],[]) |
|
296 | mkQuasiGraph lessList = |
|
297 let |
|
298 fun buildGraphs ([],leG, neqE) = (leG, neqE) |
|
299 | buildGraphs (l::ls, leG, neqE) = case l of |
|
300 (Less (x,y,p)) => |
|
301 let |
|
302 val leEdge = Le (x,y, Thm ([p], Less.less_imp_le)) |
|
303 val neqEdges = [ NotEq (x,y, Thm ([p], Less.less_imp_neq)), |
|
304 NotEq (y,x, Thm ( [Thm ([p], Less.less_imp_neq)], @{thm not_sym}))] |
|
305 in |
|
306 buildGraphs (ls, addEdge(y,[],(addEdge (x,[(y,leEdge)],leG))), neqEdges@neqE) |
|
307 end |
|
308 | (Le (x,y,p)) => buildGraphs (ls, addEdge(y,[],(addEdge (x,[(y,l)],leG))), neqE) |
|
309 | _ => buildGraphs (ls, leG, l::neqE) ; |
|
310 |
|
311 in buildGraphs (lessList, [], []) end; |
|
312 |
|
313 (* ********************************************************************** *) |
|
314 (* *) |
|
315 (* mkGraph constructs from a list of objects of type less a graph g *) |
|
316 (* Used for plain transitivity chain reasoning. *) |
|
317 (* *) |
|
318 (* ********************************************************************** *) |
|
319 |
|
320 fun mkGraph [] = [] |
|
321 | mkGraph lessList = |
|
322 let |
|
323 fun buildGraph ([],g) = g |
|
324 | buildGraph (l::ls, g) = buildGraph (ls, (addEdge ((lower l),[((upper l),l)],g))) |
|
325 |
|
326 in buildGraph (lessList, []) end; |
|
327 |
|
328 (* *********************************************************************** *) |
|
329 (* *) |
|
330 (* adjacent g u : (''a * 'b list ) list -> ''a -> 'b list *) |
|
331 (* *) |
|
332 (* List of successors of u in graph g *) |
|
333 (* *) |
|
334 (* *********************************************************************** *) |
|
335 |
|
336 fun adjacent eq_comp ((v,adj)::el) u = |
|
337 if eq_comp (u, v) then adj else adjacent eq_comp el u |
|
338 | adjacent _ [] _ = [] |
|
339 |
|
340 (* *********************************************************************** *) |
|
341 (* *) |
|
342 (* dfs eq_comp g u v: *) |
|
343 (* ('a * 'a -> bool) -> ('a *( 'a * less) list) list -> *) |
|
344 (* 'a -> 'a -> (bool * ('a * less) list) *) |
|
345 (* *) |
|
346 (* Depth first search of v from u. *) |
|
347 (* Returns (true, path(u, v)) if successful, otherwise (false, []). *) |
|
348 (* *) |
|
349 (* *********************************************************************** *) |
|
350 |
|
351 fun dfs eq_comp g u v = |
|
352 let |
|
353 val pred = Unsynchronized.ref []; |
|
354 val visited = Unsynchronized.ref []; |
|
355 |
|
356 fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited) |
|
357 |
|
358 fun dfs_visit u' = |
|
359 let val _ = visited := u' :: (!visited) |
|
360 |
|
361 fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end; |
|
362 |
|
363 in if been_visited v then () |
|
364 else (List.app (fn (v',l) => if been_visited v' then () else ( |
|
365 update (v',l); |
|
366 dfs_visit v'; ()) )) (adjacent eq_comp g u') |
|
367 end |
|
368 in |
|
369 dfs_visit u; |
|
370 if (been_visited v) then (true, (!pred)) else (false , []) |
|
371 end; |
|
372 |
|
373 (* ************************************************************************ *) |
|
374 (* *) |
|
375 (* Begin: Quasi Order relevant functions *) |
|
376 (* *) |
|
377 (* *) |
|
378 (* ************************************************************************ *) |
|
379 |
|
380 (* ************************************************************************ *) |
|
381 (* *) |
|
382 (* findPath x y g: Term.term -> Term.term -> *) |
|
383 (* (Term.term * (Term.term * less list) list) -> *) |
|
384 (* (bool, less list) *) |
|
385 (* *) |
|
386 (* Searches a path from vertex x to vertex y in Graph g, returns true and *) |
|
387 (* the list of edges forming the path, if a path is found, otherwise false *) |
|
388 (* and nil. *) |
|
389 (* *) |
|
390 (* ************************************************************************ *) |
|
391 |
|
392 |
|
393 fun findPath x y g = |
|
394 let |
|
395 val (found, tmp) = dfs (op aconv) g x y ; |
|
396 val pred = map snd tmp; |
|
397 |
|
398 fun path x y = |
|
399 let |
|
400 (* find predecessor u of node v and the edge u -> v *) |
|
401 fun lookup v [] = raise Cannot |
|
402 | lookup v (e::es) = if (upper e) aconv v then e else lookup v es; |
|
403 |
|
404 (* traverse path backwards and return list of visited edges *) |
|
405 fun rev_path v = |
|
406 let val l = lookup v pred |
|
407 val u = lower l; |
|
408 in |
|
409 if u aconv x then [l] else (rev_path u) @ [l] |
|
410 end |
|
411 in rev_path y end; |
|
412 |
|
413 in |
|
414 if found then ( |
|
415 if x aconv y then (found,[(Le (x, y, (Thm ([], Less.le_refl))))]) |
|
416 else (found, (path x y) )) |
|
417 else (found,[]) |
|
418 end; |
|
419 |
|
420 |
|
421 (* ************************************************************************ *) |
|
422 (* *) |
|
423 (* findQuasiProof (leqG, neqE) subgoal: *) |
|
424 (* (Term.term * (Term.term * less list) list) * less list -> less -> proof *) |
|
425 (* *) |
|
426 (* Constructs a proof for subgoal by searching a special path in leqG and *) |
|
427 (* neqE. Raises Cannot if construction of the proof fails. *) |
|
428 (* *) |
|
429 (* ************************************************************************ *) |
|
430 |
|
431 |
|
432 (* As the conlusion can be either of form x <= y, x < y or x ~= y we have *) |
|
433 (* three cases to deal with. Finding a transitivity path from x to y with label *) |
|
434 (* 1. <= *) |
|
435 (* This is simply done by searching any path from x to y in the graph leG. *) |
|
436 (* The graph leG contains only edges with label <=. *) |
|
437 (* *) |
|
438 (* 2. < *) |
|
439 (* A path from x to y with label < can be found by searching a path with *) |
|
440 (* label <= from x to y in the graph leG and merging the path x <= y with *) |
|
441 (* a parallel edge x ~= y resp. y ~= x to x < y. *) |
|
442 (* *) |
|
443 (* 3. ~= *) |
|
444 (* If the conclusion is of form x ~= y, we can find a proof either directly, *) |
|
445 (* if x ~= y or y ~= x are among the assumptions, or by constructing x ~= y if *) |
|
446 (* x < y or y < x follows from the assumptions. *) |
|
447 |
|
448 fun findQuasiProof (leG, neqE) subgoal = |
|
449 case subgoal of (Le (x,y, _)) => ( |
|
450 let |
|
451 val (xyLefound,xyLePath) = findPath x y leG |
|
452 in |
|
453 if xyLefound then ( |
|
454 let |
|
455 val Le_x_y = (transPath (tl xyLePath, hd xyLePath)) |
|
456 in getprf Le_x_y end ) |
|
457 else raise Cannot |
|
458 end ) |
|
459 | (Less (x,y,_)) => ( |
|
460 let |
|
461 fun findParallelNeq [] = NONE |
|
462 | findParallelNeq (e::es) = |
|
463 if (x aconv (lower e) andalso y aconv (upper e)) then SOME e |
|
464 else if (y aconv (lower e) andalso x aconv (upper e)) |
|
465 then SOME (NotEq (x,y, (Thm ([getprf e], @{thm not_sym})))) |
|
466 else findParallelNeq es; |
|
467 in |
|
468 (* test if there is a edge x ~= y respectivly y ~= x and *) |
|
469 (* if it possible to find a path x <= y in leG, thus we can conclude x < y *) |
|
470 (case findParallelNeq neqE of (SOME e) => |
|
471 let |
|
472 val (xyLeFound,xyLePath) = findPath x y leG |
|
473 in |
|
474 if xyLeFound then ( |
|
475 let |
|
476 val Le_x_y = (transPath (tl xyLePath, hd xyLePath)) |
|
477 val Less_x_y = mergeLess (e, Le_x_y) |
|
478 in getprf Less_x_y end |
|
479 ) else raise Cannot |
|
480 end |
|
481 | _ => raise Cannot) |
|
482 end ) |
|
483 | (NotEq (x,y,_)) => |
|
484 (* First check if a single premiss is sufficient *) |
|
485 (case (find_first (fn fact => fact subsumes subgoal) neqE, subgoal) of |
|
486 (SOME (NotEq (x, y, p)), NotEq (x', y', _)) => |
|
487 if (x aconv x' andalso y aconv y') then p |
|
488 else Thm ([p], @{thm not_sym}) |
|
489 | _ => raise Cannot |
|
490 ) |
|
491 |
|
492 |
|
493 (* ************************************************************************ *) |
|
494 (* *) |
|
495 (* End: Quasi Order relevant functions *) |
|
496 (* *) |
|
497 (* *) |
|
498 (* ************************************************************************ *) |
|
499 |
|
500 (* *********************************************************************** *) |
|
501 (* *) |
|
502 (* solveLeTrans sign (asms,concl) : *) |
|
503 (* theory -> less list * Term.term -> proof list *) |
|
504 (* *) |
|
505 (* Solves *) |
|
506 (* *) |
|
507 (* *********************************************************************** *) |
|
508 |
|
509 fun solveLeTrans thy (asms, concl) = |
|
510 let |
|
511 val g = mkGraph asms |
|
512 in |
|
513 let |
|
514 val (subgoal, prf) = mkconcl_trans thy concl |
|
515 val (found, path) = findPath (lower subgoal) (upper subgoal) g |
|
516 in |
|
517 if found then [getprf (transPath (tl path, hd path))] |
|
518 else raise Cannot |
|
519 end |
|
520 end; |
|
521 |
|
522 |
|
523 (* *********************************************************************** *) |
|
524 (* *) |
|
525 (* solveQuasiOrder sign (asms,concl) : *) |
|
526 (* theory -> less list * Term.term -> proof list *) |
|
527 (* *) |
|
528 (* Find proof if possible for quasi order. *) |
|
529 (* *) |
|
530 (* *********************************************************************** *) |
|
531 |
|
532 fun solveQuasiOrder thy (asms, concl) = |
|
533 let |
|
534 val (leG, neqE) = mkQuasiGraph asms |
|
535 in |
|
536 let |
|
537 val (subgoals, prf) = mkconcl_quasi thy concl |
|
538 fun solve facts less = |
|
539 (case triv_solv less of NONE => findQuasiProof (leG, neqE) less |
|
540 | SOME prf => prf ) |
|
541 in map (solve asms) subgoals end |
|
542 end; |
|
543 |
|
544 (* ************************************************************************ *) |
|
545 (* *) |
|
546 (* Tactics *) |
|
547 (* *) |
|
548 (* - trans_tac *) |
|
549 (* - quasi_tac, solves quasi orders *) |
|
550 (* ************************************************************************ *) |
|
551 |
|
552 |
|
553 (* trans_tac - solves transitivity chains over <= *) |
|
554 |
|
555 fun trans_tac ctxt = SUBGOAL (fn (A, n) => fn st => |
|
556 let |
|
557 val thy = Proof_Context.theory_of ctxt; |
|
558 val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A)); |
|
559 val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A); |
|
560 val C = subst_bounds (rfrees, Logic.strip_assums_concl A); |
|
561 val lesss = flat (map_index (mkasm_trans thy o swap) Hs); |
|
562 val prfs = solveLeTrans thy (lesss, C); |
|
563 |
|
564 val (subgoal, prf) = mkconcl_trans thy C; |
|
565 in |
|
566 Subgoal.FOCUS (fn {context = ctxt', prems, ...} => |
|
567 let val thms = map (prove prems) prfs |
|
568 in resolve_tac ctxt' [prove thms prf] 1 end) ctxt n st |
|
569 end |
|
570 handle Contr p => |
|
571 Subgoal.FOCUS (fn {context = ctxt', prems, ...} => |
|
572 resolve_tac ctxt' [prove prems p] 1) ctxt n st |
|
573 | Cannot => Seq.empty); |
|
574 |
|
575 |
|
576 (* quasi_tac - solves quasi orders *) |
|
577 |
|
578 fun quasi_tac ctxt = SUBGOAL (fn (A, n) => fn st => |
|
579 let |
|
580 val thy = Proof_Context.theory_of ctxt |
|
581 val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A)); |
|
582 val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A); |
|
583 val C = subst_bounds (rfrees, Logic.strip_assums_concl A); |
|
584 val lesss = flat (map_index (mkasm_quasi thy o swap) Hs); |
|
585 val prfs = solveQuasiOrder thy (lesss, C); |
|
586 val (subgoals, prf) = mkconcl_quasi thy C; |
|
587 in |
|
588 Subgoal.FOCUS (fn {context = ctxt', prems, ...} => |
|
589 let val thms = map (prove prems) prfs |
|
590 in resolve_tac ctxt' [prove thms prf] 1 end) ctxt n st |
|
591 end |
|
592 handle Contr p => |
|
593 (Subgoal.FOCUS (fn {context = ctxt', prems, ...} => |
|
594 resolve_tac ctxt' [prove prems p] 1) ctxt n st handle General.Subscript => Seq.empty) |
|
595 | Cannot => Seq.empty |
|
596 | General.Subscript => Seq.empty); |
|
597 |
|
598 end; |