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)+
```