unfold theorems for trancl and rtrancl
authorpaulson
Mon Feb 28 13:10:36 2005 +0100 (2005-02-28)
changeset 15551af78481b37bf
parent 15550 806214035275
child 15552 8ab8e425410b
unfold theorems for trancl and rtrancl
src/HOL/Transitive_Closure.thy
     1.1 --- a/src/HOL/Transitive_Closure.thy	Sun Feb 27 00:00:40 2005 +0100
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Mon Feb 28 13:10:36 2005 +0100
     1.3 @@ -212,6 +212,9 @@
     1.4    by (blast elim: rtranclE converse_rtranclE
     1.5      intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl)
     1.6  
     1.7 +lemma rtrancl_unfold: "r^* = Id Un (r O r^*)"
     1.8 +  by (auto intro: rtrancl_into_rtrancl elim: rtranclE)
     1.9 +
    1.10  
    1.11  subsection {* Transitive closure *}
    1.12  
    1.13 @@ -269,6 +272,9 @@
    1.14  
    1.15  inductive_cases tranclE: "(a, b) : r^+"
    1.16  
    1.17 +lemma trancl_unfold: "r^+ = r Un (r O r^+)"
    1.18 +  by (auto intro: trancl_into_trancl elim: tranclE)
    1.19 +
    1.20  lemma trans_trancl: "trans(r^+)"
    1.21    -- {* Transitivity of @{term "r^+"} *}
    1.22  proof (rule transI)
    1.23 @@ -447,6 +453,10 @@
    1.24  declare rtranclE [cases set: rtrancl]
    1.25  declare tranclE [cases set: trancl]
    1.26  
    1.27 +
    1.28 +
    1.29 +
    1.30 +
    1.31  subsection {* Setup of transitivity reasoner *}
    1.32  
    1.33  use "../Provers/trancl.ML";