src/Provers/quasi.ML
 author wenzelm Mon Mar 19 21:10:33 2012 +0100 (2012-03-19) changeset 47022 8eac39af4ec0 parent 43278 1fbdcebb364b child 58839 ccda99401bc8 permissions -rw-r--r--
moved some legacy stuff;
1 (*  Title:      Provers/quasi.ML
2     Author:     Oliver Kutter, TU Muenchen
4 Reasoner for simple transitivity and quasi orders.
5 *)
7 (*
9 The package provides tactics trans_tac and quasi_tac that use
10 premises of the form
12   t = u, t ~= u, t < u and t <= u
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.
20 Details:
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.
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 *)
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 *)
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 *)
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 *)
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 *)
55   (* Additional theorem for goals of form x ~= y *)
56   val less_imp_neq : thm (* x < y ==> x ~= y *)
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;
68 signature QUASI_TAC =
69 sig
70   val trans_tac: Proof.context -> int -> tactic
71   val quasi_tac: Proof.context -> int -> tactic
72 end;
74 functor Quasi_Tac(Less: LESS_ARITH): QUASI_TAC =
75 struct
77 (* Internal datatype for the proof *)
78 datatype proof
79   = Asm of int
80   | Thm of proof list * thm;
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 *)
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;
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;
100  (* Misc functions for datatype less *)
101 fun lower (Less (x, _, _)) = x
102   | lower (Le (x, _, _)) = x
103   | lower (NotEq (x,_,_)) = x;
105 fun upper (Less (_, y, _)) = y
106   | upper (Le (_, y, _)) = y
107   | upper (NotEq (_,y,_)) = y;
109 fun getprf   (Less (_, _, p)) = p
110 |   getprf   (Le   (_, _, p)) = p
111 |   getprf   (NotEq (_,_, p)) = p;
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 (* ************************************************************************ *)
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 => [];
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 (* ************************************************************************ *)
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 => [];
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 (* ************************************************************************ *)
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;
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 (* ************************************************************************ *)
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;
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 (* ******************************************************************* *)
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";
222 (* ******************************************************************** *)
223 (* tr checks for valid transitivity step                                *)
224 (* ******************************************************************** *)
226 infix tr;
227 fun (Le (_, y, _))   tr (Le (x', _, _))   = ( y aconv x' )
228   | _ tr _ = false;
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 (* ******************************************************************* *)
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";
246 (* ******************************************************************* *)
247 (*                                                                     *)
248 (* less1 subsumes less2 : less -> less -> bool                         *)
249 (*                                                                     *)
250 (* subsumes checks whether less1 implies less2                         *)
251 (*                                                                     *)
252 (* ******************************************************************* *)
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;
262 (* ******************************************************************* *)
263 (*                                                                     *)
264 (* triv_solv less1 : less ->  proof option                     *)
265 (*                                                                     *)
266 (* Solves trivial goal x <= x.                                         *)
267 (*                                                                     *)
268 (* ******************************************************************* *)
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;
275 (* ********************************************************************* *)
276 (* Graph functions                                                       *)
277 (* ********************************************************************* *)
279 (* *********************************************************** *)
280 (* Functions for constructing graphs                           *)
281 (* *********************************************************** *)
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));
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 (* ********************************************************************** *)
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
307          end
308      |  (Le (x,y,p))   => buildGraphs (ls, addEdge(y,[],(addEdge (x,[(y,l)],leG))), neqE)
309      | _ =>  buildGraphs (ls, leG,  l::neqE) ;
311 in buildGraphs (lessList, [],  []) end;
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 (* ********************************************************************** *)
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)))
326 in buildGraph (lessList, []) end;
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 (* *********************************************************************** *)
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 _  []  _ = []
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 (* *********************************************************************** *)
351 fun dfs eq_comp g u v =
352  let
353     val pred = Unsynchronized.ref [];
354     val visited = Unsynchronized.ref [];
356     fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
358     fun dfs_visit u' =
359     let val _ = visited := u' :: (!visited)
361     fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end;
363     in if been_visited v then ()
364     else (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;
373 (* ************************************************************************ *)
374 (*                                                                          *)
375 (* Begin: Quasi Order relevant functions                                    *)
376 (*                                                                          *)
377 (*                                                                          *)
378 (* ************************************************************************ *)
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 (* ************************************************************************ *)
393  fun findPath x y g =
394   let
395     val (found, tmp) =  dfs (op aconv) g x y ;
396     val pred = map snd tmp;
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;
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;
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;
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 (* ************************************************************************ *)
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.                                *)
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 (Library.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   )
493 (* ************************************************************************ *)
494 (*                                                                          *)
495 (* End: Quasi Order relevant functions                                      *)
496 (*                                                                          *)
497 (*                                                                          *)
498 (* ************************************************************************ *)
500 (* *********************************************************************** *)
501 (*                                                                         *)
502 (* solveLeTrans sign (asms,concl) :                                        *)
503 (* theory -> less list * Term.term -> proof list                           *)
504 (*                                                                         *)
505 (* Solves                                                                  *)
506 (*                                                                         *)
507 (* *********************************************************************** *)
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;
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 (* *********************************************************************** *)
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;
544 (* ************************************************************************ *)
545 (*                                                                          *)
546 (* Tactics                                                                  *)
547 (*                                                                          *)
548 (*  - trans_tac                                                          *)
549 (*  - quasi_tac, solves quasi orders                                        *)
550 (* ************************************************************************ *)
553 (* trans_tac - solves transitivity chains over <= *)
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);
564   val (subgoal, prf) = mkconcl_trans thy C;
565  in
566   Subgoal.FOCUS (fn {prems, ...} =>
567     let val thms = map (prove prems) prfs
568     in rtac (prove thms prf) 1 end) ctxt n st
569  end
570  handle Contr p => Subgoal.FOCUS (fn {prems, ...} => rtac (prove prems p) 1) ctxt n st
571   | Cannot  => Seq.empty);
574 (* quasi_tac - solves quasi orders *)
576 fun quasi_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
577  let
578   val thy = Proof_Context.theory_of ctxt
579   val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A));
580   val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A);
581   val C = subst_bounds (rfrees, Logic.strip_assums_concl A);
582   val lesss = flat (map_index (mkasm_quasi thy o swap) Hs);
583   val prfs = solveQuasiOrder thy (lesss, C);
584   val (subgoals, prf) = mkconcl_quasi thy C;
585  in
586   Subgoal.FOCUS (fn {prems, ...} =>
587     let val thms = map (prove prems) prfs
588     in rtac (prove thms prf) 1 end) ctxt n st
589  end
590  handle Contr p =>
591     (Subgoal.FOCUS (fn {prems, ...} => rtac (prove prems p) 1) ctxt n st
592       handle General.Subscript => Seq.empty)
593   | Cannot => Seq.empty
594   | General.Subscript => Seq.empty);
596 end;