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