# HG changeset patch
# User nipkow
# Date 800523307 -7200
# Node ID 20b708827030581f502bb495762dee0a1db714fb
# Parent  485b49694253089370a283f7b42dfd4f9d92004d
renamed trans_rtrancl to rtrancl_trans and modified it by expanding trans.

diff -r 485b49694253 -r 20b708827030 src/HOL/Trancl.ML
--- a/src/HOL/Trancl.ML	Sat May 13 14:08:24 1995 +0200
+++ b/src/HOL/Trancl.ML	Mon May 15 09:35:07 1995 +0200
@@ -139,11 +139,10 @@
 qed "rtrancl_induct";
 
 (*transitivity of transitive closure!! -- by induction.*)
-goal Trancl.thy "trans(r^*)";
-by (rtac transI 1);
-by (res_inst_tac [("b","z")] rtrancl_induct 1);
-by (DEPTH_SOLVE (eresolve_tac [asm_rl, rtrancl_into_rtrancl] 1));
-qed "trans_rtrancl";
+goal Trancl.thy "!!r. [| (a,b):r^*; (b,c):r^* |] ==> (a,c):r^*";
+by (eres_inst_tac [("b","c")] rtrancl_induct 1);
+by(ALLGOALS(fast_tac (HOL_cs addIs [rtrancl_into_rtrancl])));
+qed "rtrancl_trans";
 
 (*elimination of rtrancl -- by induction on a special formula*)
 val major::prems = goal Trancl.thy
@@ -186,7 +185,7 @@
 by (resolve_tac (prems RL [rtranclE]) 1);
 by (etac subst 1);
 by (resolve_tac (prems RL [r_into_trancl]) 1);
-by (rtac (trans_rtrancl RS transD RS rtrancl_into_trancl1) 1);
+by (rtac (rtrancl_trans RS rtrancl_into_trancl1) 1);
 by (REPEAT (ares_tac (prems@[r_into_rtrancl]) 1));
 qed "rtrancl_into_trancl2";
 
@@ -209,7 +208,7 @@
 goalw Trancl.thy [trancl_def] "trans(r^+)";
 by (rtac transI 1);
 by (REPEAT (etac compEpair 1));
-by (rtac (rtrancl_into_rtrancl RS (trans_rtrancl RS transD RS compI)) 1);
+by (rtac (rtrancl_into_rtrancl RS (rtrancl_trans RS compI)) 1);
 by (REPEAT (assume_tac 1));
 qed "trans_trancl";
 
@@ -222,11 +221,6 @@
 
 (*More about r^*)
 
-goal Trancl.thy "!!r. (b,c):r^* ==> !a. (a,b):r^* --> (a,c):r^*";
-be rtrancl_induct 1;
-by(ALLGOALS(fast_tac (comp_cs addIs [rtrancl_into_rtrancl])));
-bind_thm ("rtrancl_comp", result() RS spec RSN (2,rev_mp));
-
 goal Trancl.thy "(r^*)^* = r^*";
 br set_ext 1;
 by(res_inst_tac [("p","x")] PairE 1);
@@ -234,7 +228,7 @@
 br iffI 1;
 be rtrancl_induct 1;
 br rtrancl_refl 1;
-by(fast_tac (HOL_cs addEs [rtrancl_comp]) 1);
+by(fast_tac (HOL_cs addEs [rtrancl_trans]) 1);
 be r_into_rtrancl 1;
 qed "rtrancl_idemp";