src/HOL/Transitive_Closure.thy
changeset 19623 12e6cc4382ae
parent 19228 30fce6da8cbe
child 19656 09be06943252
     1.1 --- a/src/HOL/Transitive_Closure.thy	Fri May 12 10:38:00 2006 +0200
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Fri May 12 11:19:41 2006 +0200
     1.3 @@ -267,7 +267,7 @@
     1.4  lemma trancl_unfold: "r^+ = r Un (r O r^+)"
     1.5    by (auto intro: trancl_into_trancl elim: tranclE)
     1.6  
     1.7 -lemma trans_trancl: "trans(r^+)"
     1.8 +lemma trans_trancl[simp]: "trans(r^+)"
     1.9    -- {* Transitivity of @{term "r^+"} *}
    1.10  proof (rule transI)
    1.11    fix x y z
    1.12 @@ -278,6 +278,14 @@
    1.13  
    1.14  lemmas trancl_trans = trans_trancl [THEN transD, standard]
    1.15  
    1.16 +lemma trancl_id[simp]: "trans r \<Longrightarrow> r^+ = r"
    1.17 +apply(auto)
    1.18 +apply(erule trancl_induct)
    1.19 +apply assumption
    1.20 +apply(unfold trans_def)
    1.21 +apply(blast)
    1.22 +done
    1.23 +
    1.24  lemma rtrancl_trancl_trancl: assumes r: "(x, y) \<in> r^*"
    1.25    shows "!!z. (y, z) \<in> r^+ ==> (x, z) \<in> r^+" using r
    1.26    by induct (iprover intro: trancl_trans)+