# HG changeset patch
# User nipkow
# Date 800366904 -7200
# Node ID 485b49694253089370a283f7b42dfd4f9d92004d
# Parent  ff7dd80513e693e9253ae01d4529aed6e31e51a2
Added some lemmas about r^*.

diff -r ff7dd80513e6 -r 485b49694253 src/HOL/Trancl.ML
--- a/src/HOL/Trancl.ML	Sat May 13 13:46:48 1995 +0200
+++ b/src/HOL/Trancl.ML	Sat May 13 14:08:24 1995 +0200
@@ -220,6 +220,23 @@
 by (resolve_tac prems 1);
 qed "trancl_into_trancl2";
 
+(*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);
+by(hyp_subst_tac 1);
+br iffI 1;
+be rtrancl_induct 1;
+br rtrancl_refl 1;
+by(fast_tac (HOL_cs addEs [rtrancl_comp]) 1);
+be r_into_rtrancl 1;
+qed "rtrancl_idemp";
 
 val major::prems = goal Trancl.thy
     "[| (a,b) : r^*;  r <= Sigma A (%x.A) |] ==> a=b | a:A";