summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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