# HG changeset patch
# User paulson
# Date 1109592636 -3600
# Node ID af78481b37bfca122449f6d3fd51214a41357b16
# Parent  8062140352751bbe871590742c945642e71a304f
unfold theorems for trancl and rtrancl

diff -r 806214035275 -r af78481b37bf src/HOL/Transitive_Closure.thy
--- 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";