New prover for transitive and reflexive-transitive closure of relations.
authorballarin
Mon Jul 26 15:48:50 2004 +0200 (2004-07-26)
changeset 150764b3d280ef06a
parent 15075 a6cd1a454751
child 15077 89840837108e
New prover for transitive and reflexive-transitive closure of relations.
- Code in Provers/trancl.ML
- HOL: Simplifier set up to use it as solver
NEWS
src/HOL/Algebra/Group.thy
src/HOL/Algebra/UnivPoly.thy
src/HOL/IsaMakefile
src/HOL/MicroJava/Comp/CorrComp.thy
src/HOL/MicroJava/J/WellForm.thy
src/HOL/Transitive_Closure.thy
src/HOL/UNITY/Simple/Reach.thy
src/Provers/trancl.ML
     1.1 --- a/NEWS	Thu Jul 22 19:33:12 2004 +0200
     1.2 +++ b/NEWS	Mon Jul 26 15:48:50 2004 +0200
     1.3 @@ -6,6 +6,9 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 +* Provers/trancl.ML:  new transitivity reasoner for transitive and
     1.8 +  reflexive-transitive closure of relations.
     1.9 +
    1.10  * Pure: considerably improved version of 'constdefs' command.  Now
    1.11    performs automatic type-inference of declared constants; additional
    1.12    support for local structure declarations (cf. locales and HOL
    1.13 @@ -184,6 +187,12 @@
    1.14    Function 'Summation' over nat is gone, its syntax '\<Sum>i<k. e'
    1.15    now translates into 'setsum' as above.
    1.16  
    1.17 +* Simplifier:
    1.18 +  - Is now set up to reason about transitivity chains involving "trancl" (r^+)
    1.19 +    and "rtrancl" (r^*) by setting up tactics provided by Provers/trancl.ML
    1.20 +    as additional solvers.
    1.21 +  - INCOMPATIBILITY: old proofs break occasionally.  Typically, this is
    1.22 +    because simplification now solves more goals than previously.
    1.23  
    1.24  *** HOLCF ***
    1.25  
     2.1 --- a/src/HOL/Algebra/Group.thy	Thu Jul 22 19:33:12 2004 +0200
     2.2 +++ b/src/HOL/Algebra/Group.thy	Mon Jul 26 15:48:50 2004 +0200
     2.3 @@ -540,7 +540,7 @@
     2.4  
     2.5  
     2.6  text{*Basis for homomorphism proofs: we assume two groups @{term G} and
     2.7 -  @term{H}, with a homomorphism @{term h} between them*}
     2.8 +  @{term H}, with a homomorphism @{term h} between them*}
     2.9  locale group_hom = group G + group H + var h +
    2.10    assumes homh: "h \<in> hom G H"
    2.11    notes hom_mult [simp] = hom_mult [OF homh]
    2.12 @@ -553,7 +553,7 @@
    2.13  lemma (in group_hom) hom_one [simp]:
    2.14    "h \<one> = \<one>\<^bsub>H\<^esub>"
    2.15  proof -
    2.16 -  have "h \<one> \<otimes>\<^bsub>H\<^esub> \<one>\<^bsub>H\<^esub> = h \<one> \<otimes>\<^sub>2 h \<one>"
    2.17 +  have "h \<one> \<otimes>\<^bsub>H\<^esub> \<one>\<^bsub>H\<^esub> = h \<one> \<otimes>\<^bsub>H\<^esub> h \<one>"
    2.18      by (simp add: hom_mult [symmetric] del: hom_mult)
    2.19    then show ?thesis by (simp del: r_one)
    2.20  qed
     3.1 --- a/src/HOL/Algebra/UnivPoly.thy	Thu Jul 22 19:33:12 2004 +0200
     3.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Mon Jul 26 15:48:50 2004 +0200
     3.3 @@ -1162,7 +1162,7 @@
     3.4      next
     3.5        case (Suc j)
     3.6        (* The following could be simplified if there was a reasoner for
     3.7 -        total orders integrated with simip. *)
     3.8 +        total orders integrated with simp. *)
     3.9        have R6: "!!i k. [| k <= j; i <= Suc j - k |] ==> g i \<in> carrier R"
    3.10          using Suc by (auto intro!: funcset_mem [OF Rg]) arith
    3.11        have R8: "!!i k. [| k <= Suc j; i <= k |] ==> g (k - i) \<in> carrier R"
     4.1 --- a/src/HOL/IsaMakefile	Thu Jul 22 19:33:12 2004 +0200
     4.2 +++ b/src/HOL/IsaMakefile	Mon Jul 26 15:48:50 2004 +0200
     4.3 @@ -78,6 +78,7 @@
     4.4    $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/induct_method.ML \
     4.5    $(SRC)/Provers/make_elim.ML $(SRC)/Provers/order.ML \
     4.6    $(SRC)/Provers/simplifier.ML $(SRC)/Provers/splitter.ML \
     4.7 +  $(SRC)/Provers/trancl.ML \
     4.8    $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML $(SRC)/TFL/rules.ML \
     4.9    $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML \
    4.10    $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML \
     5.1 --- a/src/HOL/MicroJava/Comp/CorrComp.thy	Thu Jul 22 19:33:12 2004 +0200
     5.2 +++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Mon Jul 26 15:48:50 2004 +0200
     5.3 @@ -52,7 +52,7 @@
     5.4  done
     5.5  
     5.6  theorem exec_all_refl: "exec_all G s s"
     5.7 -by (simp only: exec_all_def, rule rtrancl_refl)
     5.8 +by (simp only: exec_all_def (* CBtrancl, rule rtrancl_refl*) )
     5.9  
    5.10  
    5.11  theorem exec_instr_in_exec_all:
     6.1 --- a/src/HOL/MicroJava/J/WellForm.thy	Thu Jul 22 19:33:12 2004 +0200
     6.2 +++ b/src/HOL/MicroJava/J/WellForm.thy	Mon Jul 26 15:48:50 2004 +0200
     6.3 @@ -316,7 +316,7 @@
     6.4  apply(  assumption)
     6.5  apply( fast)
     6.6  apply(auto dest!: wf_cdecl_supD)
     6.7 -apply(erule (1) converse_rtrancl_into_rtrancl)
     6.8 +(*CBtrancl: apply(erule (1) converse_rtrancl_into_rtrancl) *)
     6.9  done
    6.10  
    6.11  lemma is_type_rTI: "wf_mhead G sig rT ==> is_type G rT"
     7.1 --- a/src/HOL/Transitive_Closure.thy	Thu Jul 22 19:33:12 2004 +0200
     7.2 +++ b/src/HOL/Transitive_Closure.thy	Mon Jul 26 15:48:50 2004 +0200
     7.3 @@ -6,7 +6,9 @@
     7.4  
     7.5  header {* Reflexive and Transitive closure of a relation *}
     7.6  
     7.7 -theory Transitive_Closure = Inductive:
     7.8 +theory Transitive_Closure = Inductive
     7.9 +
    7.10 +files ("../Provers/trancl.ML"):
    7.11  
    7.12  text {*
    7.13    @{text rtrancl} is reflexive/transitive closure,
    7.14 @@ -444,4 +446,62 @@
    7.15  declare rtranclE [cases set: rtrancl]
    7.16  declare tranclE [cases set: trancl]
    7.17  
    7.18 +subsection {* Setup of transitivity reasoner *}
    7.19 +
    7.20 +use "../Provers/trancl.ML";
    7.21 +
    7.22 +ML_setup {*
    7.23 +
    7.24 +structure Trancl_Tac = Trancl_Tac_Fun (
    7.25 +  struct
    7.26 +    val r_into_trancl = thm "r_into_trancl";
    7.27 +    val trancl_trans  = thm "trancl_trans";
    7.28 +    val rtrancl_refl = thm "rtrancl_refl";
    7.29 +    val r_into_rtrancl = thm "r_into_rtrancl";
    7.30 +    val trancl_into_rtrancl = thm "trancl_into_rtrancl";
    7.31 +    val rtrancl_trancl_trancl = thm "rtrancl_trancl_trancl";
    7.32 +    val trancl_rtrancl_trancl = thm "trancl_rtrancl_trancl";
    7.33 +    val rtrancl_trans = thm "rtrancl_trans";
    7.34 +(*
    7.35 +  fun decomp (Trueprop $ t) = 
    7.36 +    let fun dec (Const ("op :", _) $ t1 $ t2 ) = 
    7.37 +	let fun dec1  (Const ("Pair", _) $ a $ b) =  (a,b);
    7.38 +	    fun dec2 (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*")
    7.39 +	      | dec2 (Const ("Transitive_Closure.trancl", _ ) $ r)  = (r,"r+")
    7.40 +	      | dec2 r = (r,"r");
    7.41 +	    val (a,b) = dec1 t1;
    7.42 +	    val (rel,r) = dec2 t2;
    7.43 +	in Some (a,b,rel,r) end
    7.44 +      | dec _ =  None 
    7.45 +    in dec t end;
    7.46 +*)
    7.47 +  fun decomp (Trueprop $ t) = 
    7.48 +    let fun dec (Const ("op :", _) $ (Const ("Pair", _) $ a $ b) $ rel ) = 
    7.49 +	let fun decr (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*")
    7.50 +	      | decr (Const ("Transitive_Closure.trancl", _ ) $ r)  = (r,"r+")
    7.51 +	      | decr r = (r,"r");
    7.52 +	    val (rel,r) = decr rel;
    7.53 +	in Some (a,b,rel,r) end
    7.54 +      | dec _ =  None 
    7.55 +    in dec t end;
    7.56 +  
    7.57 +  end); (* struct *)
    7.58 +
    7.59 +simpset_ref() := simpset ()
    7.60 +    addSolver (mk_solver "Trancl" (fn _ => Trancl_Tac.trancl_tac))
    7.61 +    addSolver (mk_solver "Rtrancl" (fn _ => Trancl_Tac.rtrancl_tac));
    7.62 +
    7.63 +*}
    7.64 +
    7.65 +(* Optional methods
    7.66 +
    7.67 +method_setup trancl =
    7.68 +  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (trancl_tac)) *}
    7.69 +  {* simple transitivity reasoner *}	    
    7.70 +method_setup rtrancl =
    7.71 +  {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (rtrancl_tac)) *}
    7.72 +  {* simple transitivity reasoner *}
    7.73 +
    7.74 +*)
    7.75 +
    7.76  end
     8.1 --- a/src/HOL/UNITY/Simple/Reach.thy	Thu Jul 22 19:33:12 2004 +0200
     8.2 +++ b/src/HOL/UNITY/Simple/Reach.thy	Mon Jul 26 15:48:50 2004 +0200
     8.3 @@ -75,7 +75,7 @@
     8.4  apply (unfold fixedpoint_def)
     8.5  apply (rule equalityI)
     8.6  apply (auto intro!: ext)
     8.7 - prefer 2 apply (blast intro: rtrancl_trans)
     8.8 +(* CBtrancl: prefer 2 apply (blast intro: rtrancl_trans) *)
     8.9  apply (erule rtrancl_induct, auto)
    8.10  done
    8.11  
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/Provers/trancl.ML	Mon Jul 26 15:48:50 2004 +0200
     9.3 @@ -0,0 +1,478 @@
     9.4 +(*
     9.5 +  Title:	Transitivity reasoner for partial and linear orders
     9.6 +  Id:		$Id$
     9.7 +  Author:	Oliver Kutter
     9.8 +  Copyright:	TU Muenchen
     9.9 +*)
    9.10 +
    9.11 +signature TRANCL_ARITH = 
    9.12 +sig
    9.13 +
    9.14 +  (* theorems for transitive closure *)
    9.15 +
    9.16 +  val r_into_trancl : thm
    9.17 +      (* (a,b) : r ==> (a,b) : r^+ *)
    9.18 +  val trancl_trans : thm
    9.19 +      (* [| (a,b) : r^+ ; (b,c) : r^+ |] ==> (a,c) : r^+ *)
    9.20 +
    9.21 +  (* additional theorems for reflexive-transitive closure *)
    9.22 +
    9.23 +  val rtrancl_refl : thm
    9.24 +      (* (a,a): r^* *)
    9.25 +  val r_into_rtrancl : thm
    9.26 +      (* (a,b) : r ==> (a,b) : r^* *)
    9.27 +  val trancl_into_rtrancl : thm
    9.28 +      (* (a,b) : r^+ ==> (a,b) : r^* *)
    9.29 +  val rtrancl_trancl_trancl : thm
    9.30 +      (* [| (a,b) : r^* ; (b,c) : r^+ |] ==> (a,c) : r^+ *)
    9.31 +  val trancl_rtrancl_trancl : thm
    9.32 +      (* [| (a,b) : r^+ ; (b,c) : r^* |] ==> (a,c) : r^+ *)
    9.33 +  val rtrancl_trans : thm
    9.34 +      (* [| (a,b) : r^* ; (b,c) : r^* |] ==> (a,c) : r^* *)
    9.35 +
    9.36 +  val decomp: term ->  (term * term * term * string) option 
    9.37 +
    9.38 +end;
    9.39 +
    9.40 +signature TRANCL_TAC = 
    9.41 +sig
    9.42 +  val trancl_tac: int -> tactic;
    9.43 +  val rtrancl_tac: int -> tactic;
    9.44 +end;
    9.45 +
    9.46 +functor Trancl_Tac_Fun (Cls : TRANCL_ARITH): TRANCL_TAC = 
    9.47 +struct
    9.48 +
    9.49 + 
    9.50 + datatype proof
    9.51 +  = Asm of int 
    9.52 +  | Thm of proof list * thm; 
    9.53 +
    9.54 + exception Cannot;
    9.55 +
    9.56 + fun prove asms = 
    9.57 +  let fun pr (Asm i) = nth_elem (i, asms)
    9.58 +  |       pr (Thm (prfs, thm)) = (map pr prfs) MRS thm
    9.59 +  in pr end;
    9.60 +
    9.61 +  
    9.62 +(* Internal datatype for inequalities *)
    9.63 +datatype rel 
    9.64 +   = R      of term * term * proof  (* just a unknown relation R *)
    9.65 +   | Trans  of term * term * proof  (* R^+ *)
    9.66 +   | RTrans of term * term * proof; (* R^* *)
    9.67 +   
    9.68 + (* Misc functions for datatype rel *)
    9.69 +fun lower (R (x, _, _)) = x
    9.70 +  | lower (Trans (x, _, _)) = x
    9.71 +  | lower (RTrans (x,_,_)) = x;
    9.72 +
    9.73 +fun upper (R (_, y, _)) = y
    9.74 +  | upper (Trans (_, y, _)) = y
    9.75 +  | upper (RTrans (_,y,_)) = y;
    9.76 +
    9.77 +fun getprf   (R (_, _, p)) = p
    9.78 +|   getprf   (Trans   (_, _, p)) = p
    9.79 +|   getprf   (RTrans (_,_, p)) = p; 
    9.80 + 
    9.81 +fun mkasm_trancl  Rel  (t, n) =
    9.82 +  case Cls.decomp t of
    9.83 +    Some (x, y, rel,r) => if rel aconv Rel then  
    9.84 +    
    9.85 +    (case r of
    9.86 +      "r"   => [Trans (x,y, Thm([Asm n], Cls.r_into_trancl))]
    9.87 +    | "r+"  => [Trans (x,y, Asm n)]
    9.88 +    | "r*"  => []
    9.89 +    | _     => error ("trancl_tac: unknown relation symbol"))
    9.90 +    else [] 
    9.91 +  | None => [];
    9.92 +  
    9.93 +fun mkasm_rtrancl Rel (t, n) =
    9.94 +  case Cls.decomp t of
    9.95 +   Some (x, y, rel, r) => if rel aconv Rel then
    9.96 +    (case r of
    9.97 +      "r"   => [ Trans (x,y, Thm([Asm n], Cls.r_into_trancl))]
    9.98 +    | "r+"  => [ Trans (x,y, Asm n)]
    9.99 +    | "r*"  => [ RTrans(x,y, Asm n)]
   9.100 +    | _     => error ("rtrancl_tac: unknown relation symbol" ))
   9.101 +   else [] 
   9.102 +  | None => [];
   9.103 +
   9.104 +fun mkconcl_trancl  t =
   9.105 +  case Cls.decomp t of
   9.106 +    Some (x, y, rel, r) => (case r of
   9.107 +      "r+"  => (rel, Trans (x,y, Asm ~1), Asm 0)
   9.108 +    | _     => raise Cannot)
   9.109 +  | None => raise Cannot;
   9.110 +
   9.111 +fun mkconcl_rtrancl  t =
   9.112 +  case Cls.decomp t of
   9.113 +    Some (x,  y, rel,r ) => (case r of
   9.114 +      "r+"  => (rel, Trans (x,y, Asm ~1),  Asm 0)
   9.115 +    | "r*"  => (rel, RTrans (x,y, Asm ~1), Asm 0)
   9.116 +    | _     => raise Cannot)
   9.117 +  | None => raise Cannot;
   9.118 +
   9.119 +(* trans. cls. rules *)
   9.120 +fun makeStep (Trans (a,_,p), Trans(_,c,q))  = Trans (a,c, Thm ([p,q], Cls.trancl_trans))
   9.121 +(* refl. + trans. cls. rules *)
   9.122 +|   makeStep (RTrans (a,_,p), Trans(_,c,q))  = Trans (a,c, Thm ([p,q], Cls.rtrancl_trancl_trancl))
   9.123 +|   makeStep (Trans (a,_,p), RTrans(_,c,q))  = Trans (a,c, Thm ([p,q], Cls.trancl_rtrancl_trancl))   
   9.124 +|   makeStep (RTrans (a,_,p), RTrans(_,c,q))  = RTrans (a,c, Thm ([p,q], Cls.rtrancl_trans))  
   9.125 +|   makeStep (a,b) = error ("makeStep: internal error: undefined case\n"^(makestring a) ^"\n" ^ (makestring b));
   9.126 +
   9.127 +(* ******************************************************************* *)
   9.128 +(*                                                                     *)
   9.129 +(* transPath (Clslist, Cls): (rel  list * rel) -> rel                  *)
   9.130 +(*                                                                     *)
   9.131 +(* If a path represented by a list of elements of type rel is found,   *)
   9.132 +(* this needs to be contracted to a single element of type rel.        *)
   9.133 +(* Prior to each transitivity step it is checked whether the step is   *)
   9.134 +(* valid.                                                              *)
   9.135 +(*                                                                     *)
   9.136 +(* ******************************************************************* *)
   9.137 +
   9.138 +fun transPath ([],acc) = acc
   9.139 +|   transPath (x::xs,acc) = transPath (xs, makeStep(acc,x))
   9.140 +      
   9.141 +(* ********************************************************************* *)
   9.142 +(* Graph functions                                                       *)
   9.143 +(* ********************************************************************* *)
   9.144 +
   9.145 +(* *********************************************************** *)
   9.146 +(* Functions for constructing graphs                           *)
   9.147 +(* *********************************************************** *)
   9.148 +
   9.149 +fun addEdge (v,d,[]) = [(v,d)]
   9.150 +|   addEdge (v,d,((u,dl)::el)) = if v aconv u then ((v,d@dl)::el)
   9.151 +    else (u,dl):: (addEdge(v,d,el));
   9.152 +    
   9.153 +(* ********************************************************************** *)
   9.154 +(*                                                                        *)
   9.155 +(* mkGraph constructs from a list of objects of type rel  a graph g       *)
   9.156 +(*                                                                        *)
   9.157 +(* ********************************************************************** *)
   9.158 +
   9.159 +fun mkGraph [] = ([],[])
   9.160 +|   mkGraph ys =  
   9.161 + let
   9.162 +  fun buildGraph ([],g,zs) = (g,zs)
   9.163 +  |   buildGraph (x::xs, g, zs) = 
   9.164 +        case x of (Trans (_,_,_)) => 
   9.165 +	       buildGraph (xs, addEdge((upper x), [],(addEdge ((lower x),[((upper x),x)],g))), x::zs) 
   9.166 +	| _ => buildGraph (xs, addEdge((upper x), [],(addEdge ((lower x),[((upper x),x)],g))), zs)
   9.167 +in buildGraph (ys, [], []) end;
   9.168 +
   9.169 +(* *********************************************************************** *)
   9.170 +(*                                                                         *)
   9.171 +(* adjacent g u : (''a * 'b list ) list -> ''a -> 'b list                  *)
   9.172 +(*                                                                         *)
   9.173 +(* List of successors of u in graph g                                      *)
   9.174 +(*                                                                         *)
   9.175 +(* *********************************************************************** *)
   9.176 + 
   9.177 +fun adjacent eq_comp ((v,adj)::el) u = 
   9.178 +    if eq_comp (u, v) then adj else adjacent eq_comp el u
   9.179 +|   adjacent _  []  _ = []  
   9.180 +
   9.181 +(* *********************************************************************** *)
   9.182 +(*                                                                         *)
   9.183 +(* dfs eq_comp g u v:                                                      *)
   9.184 +(* ('a * 'a -> bool) -> ('a  *( 'a * rel) list) list ->                    *)
   9.185 +(* 'a -> 'a -> (bool * ('a * rel) list)                                    *) 
   9.186 +(*                                                                         *)
   9.187 +(* Depth first search of v from u.                                         *)
   9.188 +(* Returns (true, path(u, v)) if successful, otherwise (false, []).        *)
   9.189 +(*                                                                         *)
   9.190 +(* *********************************************************************** *)
   9.191 +
   9.192 +fun dfs eq_comp g u v = 
   9.193 + let 
   9.194 +    val pred = ref nil;
   9.195 +    val visited = ref nil;
   9.196 +    
   9.197 +    fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
   9.198 +    
   9.199 +    fun dfs_visit u' = 
   9.200 +    let val _ = visited := u' :: (!visited)
   9.201 +    
   9.202 +    fun update (x,l) = let val _ = pred := (x,l) ::(!pred) in () end;
   9.203 +    
   9.204 +    in if been_visited v then () 
   9.205 +    else (app (fn (v',l) => if been_visited v' then () else (
   9.206 +       update (v',l); 
   9.207 +       dfs_visit v'; ()) )) (adjacent eq_comp g u')
   9.208 +     end
   9.209 +  in 
   9.210 +    dfs_visit u; 
   9.211 +    if (been_visited v) then (true, (!pred)) else (false , [])   
   9.212 +  end;
   9.213 +
   9.214 +(* *********************************************************************** *)
   9.215 +(*                                                                         *)
   9.216 +(* transpose g:                                                            *)
   9.217 +(* (''a * ''a list) list -> (''a * ''a list) list                          *)
   9.218 +(*                                                                         *)
   9.219 +(* Computes transposed graph g' from g                                     *)
   9.220 +(* by reversing all edges u -> v to v -> u                                 *)
   9.221 +(*                                                                         *)
   9.222 +(* *********************************************************************** *)
   9.223 +
   9.224 +fun transpose eq_comp g =
   9.225 +  let
   9.226 +   (* Compute list of reversed edges for each adjacency list *)
   9.227 +   fun flip (u,(v,l)::el) = (v,(u,l)) :: flip (u,el)
   9.228 +     | flip (_,nil) = nil
   9.229 +   
   9.230 +   (* Compute adjacency list for node u from the list of edges
   9.231 +      and return a likewise reduced list of edges.  The list of edges
   9.232 +      is searches for edges starting from u, and these edges are removed. *)
   9.233 +   fun gather (u,(v,w)::el) =
   9.234 +    let
   9.235 +     val (adj,edges) = gather (u,el)
   9.236 +    in
   9.237 +     if eq_comp (u, v) then (w::adj,edges)
   9.238 +     else (adj,(v,w)::edges)
   9.239 +    end
   9.240 +   | gather (_,nil) = (nil,nil)
   9.241 +
   9.242 +   (* For every node in the input graph, call gather to find all reachable
   9.243 +      nodes in the list of edges *)
   9.244 +   fun assemble ((u,_)::el) edges =
   9.245 +       let val (adj,edges) = gather (u,edges)
   9.246 +       in (u,adj) :: assemble el edges
   9.247 +       end
   9.248 +     | assemble nil _ = nil
   9.249 +
   9.250 +   (* Compute, for each adjacency list, the list with reversed edges,
   9.251 +      and concatenate these lists. *)
   9.252 +   val flipped = foldr (op @) ((map flip g),nil)
   9.253 + 
   9.254 + in assemble g flipped end    
   9.255 + 
   9.256 +(* *********************************************************************** *)
   9.257 +(*                                                                         *)
   9.258 +(* dfs_reachable eq_comp g u:                                              *)
   9.259 +(* (int * int list) list -> int -> int list                                *) 
   9.260 +(*                                                                         *)
   9.261 +(* Computes list of all nodes reachable from u in g.                       *)
   9.262 +(*                                                                         *)
   9.263 +(* *********************************************************************** *)
   9.264 +
   9.265 +fun dfs_reachable eq_comp g u = 
   9.266 + let
   9.267 +  (* List of vertices which have been visited. *)
   9.268 +  val visited  = ref nil;
   9.269 +  
   9.270 +  fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
   9.271 +
   9.272 +  fun dfs_visit g u  =
   9.273 +      let
   9.274 +   val _ = visited := u :: !visited
   9.275 +   val descendents =
   9.276 +       foldr (fn ((v,l),ds) => if been_visited v then ds
   9.277 +            else v :: dfs_visit g v @ ds)
   9.278 +        ( ((adjacent eq_comp g u)) ,nil)
   9.279 +   in  descendents end
   9.280 + 
   9.281 + in u :: dfs_visit g u end;
   9.282 +
   9.283 +(* *********************************************************************** *)
   9.284 +(*                                                                         *)
   9.285 +(* dfs_term_reachable g u:                                                  *)
   9.286 +(* (term * term list) list -> term -> term list                            *) 
   9.287 +(*                                                                         *)
   9.288 +(* Computes list of all nodes reachable from u in g.                       *)
   9.289 +(*                                                                         *)
   9.290 +(* *********************************************************************** *)
   9.291 +
   9.292 +fun dfs_term_reachable g u = dfs_reachable (op aconv) g u;
   9.293 +
   9.294 +(* ************************************************************************ *) 
   9.295 +(*                                                                          *)
   9.296 +(* findPath x y g: Term.term -> Term.term ->                                *)
   9.297 +(*                  (Term.term * (Term.term * rel list) list) ->            *) 
   9.298 +(*                  (bool, rel list)                                        *)
   9.299 +(*                                                                          *)
   9.300 +(*  Searches a path from vertex x to vertex y in Graph g, returns true and  *)
   9.301 +(*  the list of edges of edges if path is found, otherwise false and nil.   *)
   9.302 +(*                                                                          *)
   9.303 +(* ************************************************************************ *) 
   9.304 + 
   9.305 +fun findPath x y g = 
   9.306 +  let 
   9.307 +   val (found, tmp) =  dfs (op aconv) g x y ;
   9.308 +   val pred = map snd tmp;
   9.309 +	 
   9.310 +   fun path x y  =
   9.311 +    let
   9.312 +	 (* find predecessor u of node v and the edge u -> v *)
   9.313 +		
   9.314 +      fun lookup v [] = raise Cannot
   9.315 +      |   lookup v (e::es) = if (upper e) aconv v then e else lookup v es;
   9.316 +		
   9.317 +      (* traverse path backwards and return list of visited edges *)   
   9.318 +      fun rev_path v = 
   9.319 +	let val l = lookup v pred
   9.320 +	    val u = lower l;
   9.321 +	in
   9.322 +	  if u aconv x then [l] else (rev_path u) @ [l] 
   9.323 +	end
   9.324 +       
   9.325 +    in rev_path y end;
   9.326 +		
   9.327 +   in 
   9.328 +
   9.329 +     
   9.330 +      if found then ( (found, (path x y) )) else (found,[])
   9.331 +   
   9.332 +     
   9.333 +
   9.334 +   end;
   9.335 +
   9.336 +
   9.337 +fun findRtranclProof g tranclEdges subgoal = 
   9.338 +   (* simple case first *)
   9.339 +   case subgoal of (RTrans (x,y,_)) => if x aconv y then [Thm ([], Cls.rtrancl_refl)] else (
   9.340 +     let val (found, path) = findPath (lower subgoal) (upper subgoal) g
   9.341 +     in 
   9.342 +       if found then (
   9.343 +          let val path' = (transPath (tl path, hd path))
   9.344 +	  in 
   9.345 +	   
   9.346 +	    case path' of (Trans (_,_,p)) => [Thm ([p], Cls.trancl_into_rtrancl )] 
   9.347 +	    | _ => [getprf path']
   9.348 +	   
   9.349 +	  end
   9.350 +       )
   9.351 +       else raise Cannot
   9.352 +     end
   9.353 +   )
   9.354 +   
   9.355 +| (Trans (x,y,_)) => (
   9.356 + 
   9.357 +  let
   9.358 +   val Vx = dfs_term_reachable g x;
   9.359 +   val g' = transpose (op aconv) g;
   9.360 +   val Vy = dfs_term_reachable g' y;
   9.361 +   
   9.362 +   fun processTranclEdges [] = raise Cannot
   9.363 +   |   processTranclEdges (e::es) = 
   9.364 +          if (upper e) mem Vx andalso (lower e) mem Vx
   9.365 +	  andalso (upper e) mem Vy andalso (lower e) mem Vy
   9.366 +	  then (
   9.367 +	      
   9.368 +	   
   9.369 +	    if (lower e) aconv x then (
   9.370 +	      if (upper e) aconv y then (
   9.371 +	          [(getprf e)] 
   9.372 +	      )
   9.373 +	      else (
   9.374 +	          let 
   9.375 +		    val (found,path) = findPath (upper e) y g
   9.376 +		  in
   9.377 +
   9.378 +		   if found then ( 
   9.379 +		       [getprf (transPath (path, e))]
   9.380 +		      ) else processTranclEdges es
   9.381 +		  
   9.382 +		  end 
   9.383 +	      )   
   9.384 +	    )
   9.385 +	    else if (upper e) aconv y then (
   9.386 +	       let val (xufound,xupath) = findPath x (lower e) g
   9.387 +	       in 
   9.388 +	       
   9.389 +	          if xufound then (
   9.390 +		  	    
   9.391 +		    let val xuRTranclEdge = transPath (tl xupath, hd xupath)
   9.392 +			    val xyTranclEdge = makeStep(xuRTranclEdge,e)
   9.393 +				
   9.394 +				in [getprf xyTranclEdge] end
   9.395 +				
   9.396 +	         ) else processTranclEdges es
   9.397 +	       
   9.398 +	       end
   9.399 +	    )
   9.400 +	    else ( 
   9.401 +	   
   9.402 +	        let val (xufound,xupath) = findPath x (lower e) g
   9.403 +		    val (vyfound,vypath) = findPath (upper e) y g
   9.404 +		 in 
   9.405 +		    if xufound then (
   9.406 +		         if vyfound then ( 
   9.407 +			    let val xuRTranclEdge = transPath (tl xupath, hd xupath)
   9.408 +			        val vyRTranclEdge = transPath (tl vypath, hd vypath)
   9.409 +				val xyTranclEdge = makeStep (makeStep(xuRTranclEdge,e),vyRTranclEdge)
   9.410 +				
   9.411 +				in [getprf xyTranclEdge] end
   9.412 +				
   9.413 +			 ) else processTranclEdges es
   9.414 +		    ) 
   9.415 +		    else processTranclEdges es
   9.416 +		 end
   9.417 +	    )
   9.418 +	  )
   9.419 +	  else processTranclEdges es;
   9.420 +   in processTranclEdges tranclEdges end )
   9.421 +| _ => raise Cannot
   9.422 +
   9.423 +   
   9.424 +fun solveTrancl (asms, concl) = 
   9.425 + let val (g,_) = mkGraph asms
   9.426 + in
   9.427 +  let val (_, subgoal, _) = mkconcl_trancl concl
   9.428 +      val (found, path) = findPath (lower subgoal) (upper subgoal) g
   9.429 +  in
   9.430 +
   9.431 +   
   9.432 +    if found then  [getprf (transPath (tl path, hd path))]
   9.433 +    else raise Cannot 
   9.434 +   
   9.435 +  end
   9.436 + end;
   9.437 +  
   9.438 +
   9.439 + 
   9.440 +fun solveRtrancl (asms, concl) = 
   9.441 + let val (g,tranclEdges) = mkGraph asms
   9.442 +     val (_, subgoal, _) = mkconcl_rtrancl concl
   9.443 +in
   9.444 +  findRtranclProof g tranclEdges subgoal
   9.445 +end;
   9.446 + 
   9.447 +   
   9.448 +val trancl_tac =   SUBGOAL (fn (A, n) =>
   9.449 + let
   9.450 +  val Hs = Logic.strip_assums_hyp A;
   9.451 +  val C = Logic.strip_assums_concl A;
   9.452 +  val (rel,subgoals, prf) = mkconcl_trancl C;
   9.453 +  val prems = flat (ListPair.map (mkasm_trancl rel) (Hs, 0 upto (length Hs - 1)))
   9.454 +  val prfs = solveTrancl (prems, C);
   9.455 +
   9.456 + in
   9.457 +  METAHYPS (fn asms =>
   9.458 +    let val thms = map (prove asms) prfs
   9.459 +    in rtac (prove thms prf) 1 end) n
   9.460 + end
   9.461 +handle  Cannot  => no_tac);
   9.462 +
   9.463 + 
   9.464 + 
   9.465 +val rtrancl_tac =   SUBGOAL (fn (A, n) =>
   9.466 + let
   9.467 +  val Hs = Logic.strip_assums_hyp A;
   9.468 +  val C = Logic.strip_assums_concl A;
   9.469 +  val (rel,subgoals, prf) = mkconcl_rtrancl C;
   9.470 +
   9.471 +  val prems = flat (ListPair.map (mkasm_rtrancl rel) (Hs, 0 upto (length Hs - 1)))
   9.472 +  val prfs = solveRtrancl (prems, C);
   9.473 + in
   9.474 +  METAHYPS (fn asms =>
   9.475 +    let val thms = map (prove asms) prfs
   9.476 +    in rtac (prove thms prf) 1 end) n
   9.477 + end
   9.478 +handle  Cannot  => no_tac);
   9.479 +
   9.480 +end;
   9.481 +