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