src/HOL/Transitive_Closure.thy
changeset 13867 1fdecd15437f
parent 13726 9550a6f4ed4a
child 14208 144f45277d5a
     1.1 --- a/src/HOL/Transitive_Closure.thy	Mon Mar 17 17:37:48 2003 +0100
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Mon Mar 17 18:38:50 2003 +0100
     1.3 @@ -341,13 +341,8 @@
     1.4    apply (blast intro: rtrancl_trans)
     1.5    done
     1.6  
     1.7 -lemma irrefl_tranclI: "r^-1 \<inter> r^+ = {} ==> (x, x) \<notin> r^+"
     1.8 -  apply (subgoal_tac "ALL y. (x, y) : r^+ --> x \<noteq> y")
     1.9 -   apply fast
    1.10 -  apply (intro strip)
    1.11 -  apply (erule trancl_induct)
    1.12 -   apply (auto intro: r_into_trancl)
    1.13 -  done
    1.14 +lemma irrefl_tranclI: "r^-1 \<inter> r^* = {} ==> (x, x) \<notin> r^+"
    1.15 +by(blast elim: tranclE dest: trancl_into_rtrancl)
    1.16  
    1.17  lemma irrefl_trancl_rD: "!!X. ALL x. (x, x) \<notin> r^+ ==> (x, y) \<in> r ==> x \<noteq> y"
    1.18    by (blast dest: r_into_trancl)