--- a/src/HOL/Trancl.ML Sat May 27 16:10:10 1995 +0200
+++ b/src/HOL/Trancl.ML Sun May 28 17:17:43 1995 +0200
@@ -149,7 +149,7 @@
by (resolve_tac prems 1);
qed "trancl_into_trancl2";
-(*More about r^*)
+(** More about r^* **)
goal Trancl.thy "(r^*)^* = r^*";
br set_ext 1;
@@ -162,6 +162,29 @@
be r_into_rtrancl 1;
qed "rtrancl_idemp";
+
+goal Trancl.thy "!!r. (x,y) : (converse r)^* ==> (x,y) : converse(r^*)";
+br converseI 1;
+be rtrancl_induct 1;
+br rtrancl_refl 1;
+by(fast_tac (rel_cs addIs [r_into_rtrancl,rtrancl_trans]) 1);
+qed "rtrancl_converseD";
+
+goal Trancl.thy "!!r. (x,y) : converse(r^*) ==> (x,y) : (converse r)^*";
+bd converseD 1;
+be rtrancl_induct 1;
+br rtrancl_refl 1;
+by(fast_tac (rel_cs addIs [r_into_rtrancl,rtrancl_trans]) 1);
+qed "rtrancl_converseI";
+
+goal Trancl.thy "(converse r)^* = converse(r^*)";
+by(safe_tac (rel_eq_cs addSIs [rtrancl_converseI]));
+by(res_inst_tac [("p","x")] PairE 1);
+by(hyp_subst_tac 1);
+be rtrancl_converseD 1;
+qed "rtrancl_converse";
+
+
val major::prems = goal Trancl.thy
"[| (a,b) : r^*; r <= Sigma A (%x.A) |] ==> a=b | a:A";
by (cut_facts_tac prems 1);
@@ -174,3 +197,5 @@
"!!r. r <= Sigma A (%x.A) ==> trancl(r) <= Sigma A (%x.A)";
by (fast_tac (rel_cs addSDs [trancl_subset_Sigma_lemma]) 1);
qed "trancl_subset_Sigma";
+
+val trancl_cs = rel_cs addIs [rtrancl_refl];