# HG changeset patch
# User oheimb
# Date 959960823 -7200
# Node ID a389be05c06ffd06c2f36480b1fd25ba181aa11a
# Parent  5643223dad0a171c8b32c9c596efad8e310a3266
added rtranclD, tranclD, irrefl_trancl_rD

diff -r 5643223dad0a -r a389be05c06f src/HOL/Trancl.ML
--- a/src/HOL/Trancl.ML	Fri Jun 02 17:47:02 2000 +0200
+++ b/src/HOL/Trancl.ML	Fri Jun 02 17:47:03 2000 +0200
@@ -238,6 +238,12 @@
 by (REPEAT (ares_tac [r_into_rtrancl] 1));
 qed "rtrancl_into_trancl2";
 
+Goal "(a, b) : R^* ==> a = b | (a, b) : R^+";
+by (etac rtranclE 1);
+by  (datac rtrancl_into_trancl1 1 2);
+by   Auto_tac;
+qed "rtranclD";
+
 (*Nice induction rule for trancl*)
 val major::prems = Goal
   "[| (a,b) : r^+;                                      \
@@ -333,6 +339,15 @@
 by (blast_tac (claset() addIs prems addSDs [trancl_converseD])1);
 qed "converse_trancl_induct";
 
+Goal "(x,y):R^+ ==> ? z. (x,z):R & (z,y):R^*";
+be converse_trancl_induct 1;
+by Auto_tac;
+br exI 1;
+be conjI 1;
+be (r_into_rtrancl RS rtrancl_trans) 1;
+ba 1;
+qed "tranclD";
+
 (*Unused*)
 Goal "r^-1 Int r^+ = {} ==> (x, x) ~: r^+";
 by (subgoal_tac "!y. (x, y) : r^+ --> x~=y" 1);
@@ -342,6 +357,10 @@
 by (auto_tac (claset() addIs [r_into_trancl], simpset()));
 qed "irrefl_tranclI";
 
+Goal "!!X. [| !x. (x, x) ~: r^+; (x,y) : r |] ==> x ~= y";
+by (blast_tac (claset() addDs [r_into_trancl]) 1);
+qed "irrefl_trancl_rD";
+
 Goal "[| (a,b) : r^*;  r <= A <*> A |] ==> a=b | a:A";
 by (etac rtrancl_induct 1);
 by Auto_tac;