src/HOL/Order_Relation.thy
 changeset 63952 354808e9f44b parent 63572 c0cbfd2b5a45 child 68484 59793df7f853
```     1.1 --- a/src/HOL/Order_Relation.thy	Mon Sep 26 07:56:54 2016 +0200
1.2 +++ b/src/HOL/Order_Relation.thy	Wed Sep 28 17:01:01 2016 +0100
1.3 @@ -397,6 +397,18 @@
1.4    ultimately show ?thesis unfolding R_def by blast
1.5  qed
1.6
1.7 +text\<open>A transitive relation is well-founded if all initial segments are finite.\<close>
1.8 +corollary wf_finite_segments:
1.9 +  assumes "irrefl r" and "trans r" and "\<And>x. finite {y. (y, x) \<in> r}"
1.10 +  shows "wf (r)"
1.11 +proof (clarsimp simp: trans_wf_iff wf_iff_acyclic_if_finite converse_def assms)
1.12 +  fix a
1.13 +  have "trans (r \<inter> ({x. (x, a) \<in> r} \<times> {x. (x, a) \<in> r}))"
1.14 +    using assms unfolding trans_def Field_def by blast
1.15 +  then show "acyclic (r \<inter> {x. (x, a) \<in> r} \<times> {x. (x, a) \<in> r})"
1.16 +    using assms acyclic_def assms irrefl_def by fastforce
1.17 +qed
1.18 +
1.19  text \<open>The next lemma is a variation of \<open>wf_eq_minimal\<close> from Wellfounded,
1.20    allowing one to assume the set included in the field.\<close>
1.21
```