src/Provers/trancl.ML
author ballarin
Mon, 26 Jul 2004 15:48:50 +0200
changeset 15076 4b3d280ef06a
child 15078 8beb68a7afd9
permissions -rw-r--r--
New prover for transitive and reflexive-transitive closure of relations. - Code in Provers/trancl.ML - HOL: Simplifier set up to use it as solver
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15076
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
     1
(*
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
     2
  Title:	Transitivity reasoner for partial and linear orders
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
     3
  Id:		$Id$
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
     4
  Author:	Oliver Kutter
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
     5
  Copyright:	TU Muenchen
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
     6
*)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
     7
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
     8
signature TRANCL_ARITH = 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
     9
sig
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    10
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    11
  (* theorems for transitive closure *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    12
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    13
  val r_into_trancl : thm
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    14
      (* (a,b) : r ==> (a,b) : r^+ *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    15
  val trancl_trans : thm
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    16
      (* [| (a,b) : r^+ ; (b,c) : r^+ |] ==> (a,c) : r^+ *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    17
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    18
  (* additional theorems for reflexive-transitive closure *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    19
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    20
  val rtrancl_refl : thm
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    21
      (* (a,a): r^* *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    22
  val r_into_rtrancl : thm
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    23
      (* (a,b) : r ==> (a,b) : r^* *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    24
  val trancl_into_rtrancl : thm
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    25
      (* (a,b) : r^+ ==> (a,b) : r^* *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    26
  val rtrancl_trancl_trancl : thm
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    27
      (* [| (a,b) : r^* ; (b,c) : r^+ |] ==> (a,c) : r^+ *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    28
  val trancl_rtrancl_trancl : thm
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    29
      (* [| (a,b) : r^+ ; (b,c) : r^* |] ==> (a,c) : r^+ *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    30
  val rtrancl_trans : thm
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    31
      (* [| (a,b) : r^* ; (b,c) : r^* |] ==> (a,c) : r^* *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    32
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    33
  val decomp: term ->  (term * term * term * string) option 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    34
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    35
end;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    36
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    37
signature TRANCL_TAC = 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    38
sig
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    39
  val trancl_tac: int -> tactic;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    40
  val rtrancl_tac: int -> tactic;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    41
end;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    42
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    43
functor Trancl_Tac_Fun (Cls : TRANCL_ARITH): TRANCL_TAC = 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    44
struct
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    45
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    46
 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    47
 datatype proof
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    48
  = Asm of int 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    49
  | Thm of proof list * thm; 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    50
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    51
 exception Cannot;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    52
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    53
 fun prove asms = 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    54
  let fun pr (Asm i) = nth_elem (i, asms)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    55
  |       pr (Thm (prfs, thm)) = (map pr prfs) MRS thm
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    56
  in pr end;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    57
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    58
  
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    59
(* Internal datatype for inequalities *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    60
datatype rel 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    61
   = R      of term * term * proof  (* just a unknown relation R *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    62
   | Trans  of term * term * proof  (* R^+ *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    63
   | RTrans of term * term * proof; (* R^* *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    64
   
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    65
 (* Misc functions for datatype rel *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    66
fun lower (R (x, _, _)) = x
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    67
  | lower (Trans (x, _, _)) = x
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    68
  | lower (RTrans (x,_,_)) = x;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    69
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    70
fun upper (R (_, y, _)) = y
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    71
  | upper (Trans (_, y, _)) = y
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    72
  | upper (RTrans (_,y,_)) = y;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    73
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    74
fun getprf   (R (_, _, p)) = p
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    75
|   getprf   (Trans   (_, _, p)) = p
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    76
|   getprf   (RTrans (_,_, p)) = p; 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    77
 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    78
fun mkasm_trancl  Rel  (t, n) =
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    79
  case Cls.decomp t of
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    80
    Some (x, y, rel,r) => if rel aconv Rel then  
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    81
    
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    82
    (case r of
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    83
      "r"   => [Trans (x,y, Thm([Asm n], Cls.r_into_trancl))]
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    84
    | "r+"  => [Trans (x,y, Asm n)]
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    85
    | "r*"  => []
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    86
    | _     => error ("trancl_tac: unknown relation symbol"))
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    87
    else [] 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    88
  | None => [];
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    89
  
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    90
fun mkasm_rtrancl Rel (t, n) =
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    91
  case Cls.decomp t of
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    92
   Some (x, y, rel, r) => if rel aconv Rel then
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    93
    (case r of
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    94
      "r"   => [ Trans (x,y, Thm([Asm n], Cls.r_into_trancl))]
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    95
    | "r+"  => [ Trans (x,y, Asm n)]
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    96
    | "r*"  => [ RTrans(x,y, Asm n)]
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    97
    | _     => error ("rtrancl_tac: unknown relation symbol" ))
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    98
   else [] 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
    99
  | None => [];
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   100
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   101
fun mkconcl_trancl  t =
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   102
  case Cls.decomp t of
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   103
    Some (x, y, rel, r) => (case r of
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   104
      "r+"  => (rel, Trans (x,y, Asm ~1), Asm 0)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   105
    | _     => raise Cannot)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   106
  | None => raise Cannot;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   107
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   108
fun mkconcl_rtrancl  t =
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   109
  case Cls.decomp t of
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   110
    Some (x,  y, rel,r ) => (case r of
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   111
      "r+"  => (rel, Trans (x,y, Asm ~1),  Asm 0)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   112
    | "r*"  => (rel, RTrans (x,y, Asm ~1), Asm 0)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   113
    | _     => raise Cannot)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   114
  | None => raise Cannot;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   115
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   116
(* trans. cls. rules *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   117
fun makeStep (Trans (a,_,p), Trans(_,c,q))  = Trans (a,c, Thm ([p,q], Cls.trancl_trans))
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   118
(* refl. + trans. cls. rules *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   119
|   makeStep (RTrans (a,_,p), Trans(_,c,q))  = Trans (a,c, Thm ([p,q], Cls.rtrancl_trancl_trancl))
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   120
|   makeStep (Trans (a,_,p), RTrans(_,c,q))  = Trans (a,c, Thm ([p,q], Cls.trancl_rtrancl_trancl))   
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   121
|   makeStep (RTrans (a,_,p), RTrans(_,c,q))  = RTrans (a,c, Thm ([p,q], Cls.rtrancl_trans))  
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   122
|   makeStep (a,b) = error ("makeStep: internal error: undefined case\n"^(makestring a) ^"\n" ^ (makestring b));
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   123
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   124
(* ******************************************************************* *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   125
(*                                                                     *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   126
(* transPath (Clslist, Cls): (rel  list * rel) -> rel                  *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   127
(*                                                                     *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   128
(* If a path represented by a list of elements of type rel is found,   *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   129
(* this needs to be contracted to a single element of type rel.        *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   130
(* Prior to each transitivity step it is checked whether the step is   *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   131
(* valid.                                                              *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   132
(*                                                                     *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   133
(* ******************************************************************* *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   134
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   135
fun transPath ([],acc) = acc
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   136
|   transPath (x::xs,acc) = transPath (xs, makeStep(acc,x))
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   137
      
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   138
(* ********************************************************************* *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   139
(* Graph functions                                                       *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   140
(* ********************************************************************* *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   141
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   142
(* *********************************************************** *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   143
(* Functions for constructing graphs                           *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   144
(* *********************************************************** *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   145
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   146
fun addEdge (v,d,[]) = [(v,d)]
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   147
|   addEdge (v,d,((u,dl)::el)) = if v aconv u then ((v,d@dl)::el)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   148
    else (u,dl):: (addEdge(v,d,el));
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   149
    
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   150
(* ********************************************************************** *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   151
(*                                                                        *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   152
(* mkGraph constructs from a list of objects of type rel  a graph g       *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   153
(*                                                                        *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   154
(* ********************************************************************** *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   155
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   156
fun mkGraph [] = ([],[])
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   157
|   mkGraph ys =  
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   158
 let
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   159
  fun buildGraph ([],g,zs) = (g,zs)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   160
  |   buildGraph (x::xs, g, zs) = 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   161
        case x of (Trans (_,_,_)) => 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   162
	       buildGraph (xs, addEdge((upper x), [],(addEdge ((lower x),[((upper x),x)],g))), x::zs) 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   163
	| _ => buildGraph (xs, addEdge((upper x), [],(addEdge ((lower x),[((upper x),x)],g))), zs)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   164
in buildGraph (ys, [], []) end;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   165
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   166
(* *********************************************************************** *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   167
(*                                                                         *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   168
(* adjacent g u : (''a * 'b list ) list -> ''a -> 'b list                  *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   169
(*                                                                         *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   170
(* List of successors of u in graph g                                      *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   171
(*                                                                         *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   172
(* *********************************************************************** *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   173
 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   174
fun adjacent eq_comp ((v,adj)::el) u = 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   175
    if eq_comp (u, v) then adj else adjacent eq_comp el u
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   176
|   adjacent _  []  _ = []  
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   177
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   178
(* *********************************************************************** *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   179
(*                                                                         *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   180
(* dfs eq_comp g u v:                                                      *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   181
(* ('a * 'a -> bool) -> ('a  *( 'a * rel) list) list ->                    *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   182
(* 'a -> 'a -> (bool * ('a * rel) list)                                    *) 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   183
(*                                                                         *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   184
(* Depth first search of v from u.                                         *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   185
(* Returns (true, path(u, v)) if successful, otherwise (false, []).        *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   186
(*                                                                         *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   187
(* *********************************************************************** *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   188
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   189
fun dfs eq_comp g u v = 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   190
 let 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   191
    val pred = ref nil;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   192
    val visited = ref nil;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   193
    
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   194
    fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   195
    
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   196
    fun dfs_visit u' = 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   197
    let val _ = visited := u' :: (!visited)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   198
    
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   199
    fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   200
    
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   201
    in if been_visited v then () 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   202
    else (app (fn (v',l) => if been_visited v' then () else (
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   203
       update (v',l); 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   204
       dfs_visit v'; ()) )) (adjacent eq_comp g u')
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   205
     end
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   206
  in 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   207
    dfs_visit u; 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   208
    if (been_visited v) then (true, (!pred)) else (false , [])   
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   209
  end;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   210
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   211
(* *********************************************************************** *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   212
(*                                                                         *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   213
(* transpose g:                                                            *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   214
(* (''a * ''a list) list -> (''a * ''a list) list                          *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   215
(*                                                                         *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   216
(* Computes transposed graph g' from g                                     *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   217
(* by reversing all edges u -> v to v -> u                                 *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   218
(*                                                                         *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   219
(* *********************************************************************** *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   220
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   221
fun transpose eq_comp g =
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   222
  let
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   223
   (* Compute list of reversed edges for each adjacency list *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   224
   fun flip (u,(v,l)::el) = (v,(u,l)) :: flip (u,el)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   225
     | flip (_,nil) = nil
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   226
   
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   227
   (* Compute adjacency list for node u from the list of edges
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   228
      and return a likewise reduced list of edges.  The list of edges
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   229
      is searches for edges starting from u, and these edges are removed. *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   230
   fun gather (u,(v,w)::el) =
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   231
    let
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   232
     val (adj,edges) = gather (u,el)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   233
    in
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   234
     if eq_comp (u, v) then (w::adj,edges)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   235
     else (adj,(v,w)::edges)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   236
    end
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   237
   | gather (_,nil) = (nil,nil)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   238
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   239
   (* For every node in the input graph, call gather to find all reachable
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   240
      nodes in the list of edges *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   241
   fun assemble ((u,_)::el) edges =
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   242
       let val (adj,edges) = gather (u,edges)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   243
       in (u,adj) :: assemble el edges
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   244
       end
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   245
     | assemble nil _ = nil
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   246
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   247
   (* Compute, for each adjacency list, the list with reversed edges,
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   248
      and concatenate these lists. *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   249
   val flipped = foldr (op @) ((map flip g),nil)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   250
 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   251
 in assemble g flipped end    
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   252
 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   253
(* *********************************************************************** *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   254
(*                                                                         *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   255
(* dfs_reachable eq_comp g u:                                              *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   256
(* (int * int list) list -> int -> int list                                *) 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   257
(*                                                                         *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   258
(* Computes list of all nodes reachable from u in g.                       *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   259
(*                                                                         *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   260
(* *********************************************************************** *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   261
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   262
fun dfs_reachable eq_comp g u = 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   263
 let
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   264
  (* List of vertices which have been visited. *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   265
  val visited  = ref nil;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   266
  
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   267
  fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   268
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   269
  fun dfs_visit g u  =
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   270
      let
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   271
   val _ = visited := u :: !visited
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   272
   val descendents =
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   273
       foldr (fn ((v,l),ds) => if been_visited v then ds
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   274
            else v :: dfs_visit g v @ ds)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   275
        ( ((adjacent eq_comp g u)) ,nil)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   276
   in  descendents end
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   277
 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   278
 in u :: dfs_visit g u end;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   279
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   280
(* *********************************************************************** *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   281
(*                                                                         *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   282
(* dfs_term_reachable g u:                                                  *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   283
(* (term * term list) list -> term -> term list                            *) 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   284
(*                                                                         *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   285
(* Computes list of all nodes reachable from u in g.                       *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   286
(*                                                                         *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   287
(* *********************************************************************** *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   288
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   289
fun dfs_term_reachable g u = dfs_reachable (op aconv) g u;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   290
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   291
(* ************************************************************************ *) 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   292
(*                                                                          *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   293
(* findPath x y g: Term.term -> Term.term ->                                *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   294
(*                  (Term.term * (Term.term * rel list) list) ->            *) 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   295
(*                  (bool, rel list)                                        *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   296
(*                                                                          *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   297
(*  Searches a path from vertex x to vertex y in Graph g, returns true and  *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   298
(*  the list of edges of edges if path is found, otherwise false and nil.   *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   299
(*                                                                          *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   300
(* ************************************************************************ *) 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   301
 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   302
fun findPath x y g = 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   303
  let 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   304
   val (found, tmp) =  dfs (op aconv) g x y ;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   305
   val pred = map snd tmp;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   306
	 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   307
   fun path x y  =
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   308
    let
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   309
	 (* find predecessor u of node v and the edge u -> v *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   310
		
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   311
      fun lookup v [] = raise Cannot
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   312
      |   lookup v (e::es) = if (upper e) aconv v then e else lookup v es;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   313
		
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   314
      (* traverse path backwards and return list of visited edges *)   
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   315
      fun rev_path v = 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   316
	let val l = lookup v pred
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   317
	    val u = lower l;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   318
	in
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   319
	  if u aconv x then [l] else (rev_path u) @ [l] 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   320
	end
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   321
       
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   322
    in rev_path y end;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   323
		
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   324
   in 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   325
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   326
     
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   327
      if found then ( (found, (path x y) )) else (found,[])
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   328
   
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   329
     
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   330
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   331
   end;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   332
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   333
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   334
fun findRtranclProof g tranclEdges subgoal = 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   335
   (* simple case first *)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   336
   case subgoal of (RTrans (x,y,_)) => if x aconv y then [Thm ([], Cls.rtrancl_refl)] else (
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   337
     let val (found, path) = findPath (lower subgoal) (upper subgoal) g
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   338
     in 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   339
       if found then (
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   340
          let val path' = (transPath (tl path, hd path))
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   341
	  in 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   342
	   
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   343
	    case path' of (Trans (_,_,p)) => [Thm ([p], Cls.trancl_into_rtrancl )] 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   344
	    | _ => [getprf path']
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   345
	   
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   346
	  end
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   347
       )
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   348
       else raise Cannot
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   349
     end
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   350
   )
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   351
   
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   352
| (Trans (x,y,_)) => (
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   353
 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   354
  let
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   355
   val Vx = dfs_term_reachable g x;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   356
   val g' = transpose (op aconv) g;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   357
   val Vy = dfs_term_reachable g' y;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   358
   
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   359
   fun processTranclEdges [] = raise Cannot
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   360
   |   processTranclEdges (e::es) = 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   361
          if (upper e) mem Vx andalso (lower e) mem Vx
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   362
	  andalso (upper e) mem Vy andalso (lower e) mem Vy
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   363
	  then (
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   364
	      
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   365
	   
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   366
	    if (lower e) aconv x then (
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   367
	      if (upper e) aconv y then (
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   368
	          [(getprf e)] 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   369
	      )
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   370
	      else (
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   371
	          let 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   372
		    val (found,path) = findPath (upper e) y g
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   373
		  in
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   374
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   375
		   if found then ( 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   376
		       [getprf (transPath (path, e))]
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   377
		      ) else processTranclEdges es
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   378
		  
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   379
		  end 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   380
	      )   
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   381
	    )
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   382
	    else if (upper e) aconv y then (
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   383
	       let val (xufound,xupath) = findPath x (lower e) g
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   384
	       in 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   385
	       
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   386
	          if xufound then (
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   387
		  	    
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   388
		    let val xuRTranclEdge = transPath (tl xupath, hd xupath)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   389
			    val xyTranclEdge = makeStep(xuRTranclEdge,e)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   390
				
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   391
				in [getprf xyTranclEdge] end
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   392
				
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   393
	         ) else processTranclEdges es
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   394
	       
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   395
	       end
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   396
	    )
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   397
	    else ( 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   398
	   
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   399
	        let val (xufound,xupath) = findPath x (lower e) g
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   400
		    val (vyfound,vypath) = findPath (upper e) y g
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   401
		 in 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   402
		    if xufound then (
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   403
		         if vyfound then ( 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   404
			    let val xuRTranclEdge = transPath (tl xupath, hd xupath)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   405
			        val vyRTranclEdge = transPath (tl vypath, hd vypath)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   406
				val xyTranclEdge = makeStep (makeStep(xuRTranclEdge,e),vyRTranclEdge)
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   407
				
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   408
				in [getprf xyTranclEdge] end
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   409
				
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   410
			 ) else processTranclEdges es
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   411
		    ) 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   412
		    else processTranclEdges es
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   413
		 end
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   414
	    )
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   415
	  )
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   416
	  else processTranclEdges es;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   417
   in processTranclEdges tranclEdges end )
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   418
| _ => raise Cannot
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   419
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   420
   
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   421
fun solveTrancl (asms, concl) = 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   422
 let val (g,_) = mkGraph asms
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   423
 in
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   424
  let val (_, subgoal, _) = mkconcl_trancl concl
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   425
      val (found, path) = findPath (lower subgoal) (upper subgoal) g
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   426
  in
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   427
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   428
   
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   429
    if found then  [getprf (transPath (tl path, hd path))]
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   430
    else raise Cannot 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   431
   
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   432
  end
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   433
 end;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   434
  
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   435
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   436
 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   437
fun solveRtrancl (asms, concl) = 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   438
 let val (g,tranclEdges) = mkGraph asms
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   439
     val (_, subgoal, _) = mkconcl_rtrancl concl
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   440
in
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   441
  findRtranclProof g tranclEdges subgoal
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   442
end;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   443
 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   444
   
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   445
val trancl_tac =   SUBGOAL (fn (A, n) =>
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   446
 let
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   447
  val Hs = Logic.strip_assums_hyp A;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   448
  val C = Logic.strip_assums_concl A;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   449
  val (rel,subgoals, prf) = mkconcl_trancl C;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   450
  val prems = flat (ListPair.map (mkasm_trancl rel) (Hs, 0 upto (length Hs - 1)))
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   451
  val prfs = solveTrancl (prems, C);
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   452
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   453
 in
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   454
  METAHYPS (fn asms =>
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   455
    let val thms = map (prove asms) prfs
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   456
    in rtac (prove thms prf) 1 end) n
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   457
 end
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   458
handle  Cannot  => no_tac);
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   459
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   460
 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   461
 
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   462
val rtrancl_tac =   SUBGOAL (fn (A, n) =>
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   463
 let
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   464
  val Hs = Logic.strip_assums_hyp A;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   465
  val C = Logic.strip_assums_concl A;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   466
  val (rel,subgoals, prf) = mkconcl_rtrancl C;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   467
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   468
  val prems = flat (ListPair.map (mkasm_rtrancl rel) (Hs, 0 upto (length Hs - 1)))
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   469
  val prfs = solveRtrancl (prems, C);
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   470
 in
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   471
  METAHYPS (fn asms =>
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   472
    let val thms = map (prove asms) prfs
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   473
    in rtac (prove thms prf) 1 end) n
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   474
 end
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   475
handle  Cannot  => no_tac);
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   476
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   477
end;
4b3d280ef06a New prover for transitive and reflexive-transitive closure of relations.
ballarin
parents:
diff changeset
   478