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