--- a/src/HOL/Transitive_Closure.thy Sun Feb 27 00:00:40 2005 +0100
+++ b/src/HOL/Transitive_Closure.thy Mon Feb 28 13:10:36 2005 +0100
@@ -212,6 +212,9 @@
by (blast elim: rtranclE converse_rtranclE
intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl)
+lemma rtrancl_unfold: "r^* = Id Un (r O r^*)"
+ by (auto intro: rtrancl_into_rtrancl elim: rtranclE)
+
subsection {* Transitive closure *}
@@ -269,6 +272,9 @@
inductive_cases tranclE: "(a, b) : r^+"
+lemma trancl_unfold: "r^+ = r Un (r O r^+)"
+ by (auto intro: trancl_into_trancl elim: tranclE)
+
lemma trans_trancl: "trans(r^+)"
-- {* Transitivity of @{term "r^+"} *}
proof (rule transI)
@@ -447,6 +453,10 @@
declare rtranclE [cases set: rtrancl]
declare tranclE [cases set: trancl]
+
+
+
+
subsection {* Setup of transitivity reasoner *}
use "../Provers/trancl.ML";