# HG changeset patch
# User hoelzl
# Date 1384280933 -3600
# Node ID 900c6d724250a075749ff644e6024807d778feb1
# Parent  f72e58a5a75f50bb87accab7b3d1143a34a5df23
add acyclicI_order

diff -r f72e58a5a75f -r 900c6d724250 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Tue Nov 12 19:28:52 2013 +0100
+++ b/src/HOL/Transitive_Closure.thy	Tue Nov 12 19:28:53 2013 +0100
@@ -1181,6 +1181,17 @@
 lemma acyclicI: "ALL x. (x, x) ~: r^+ ==> acyclic r"
   by (simp add: acyclic_def)
 
+lemma (in order) acyclicI_order:
+  assumes *: "\<And>a b. (a, b) \<in> r \<Longrightarrow> f b < f a"
+  shows "acyclic r"
+proof -
+  { fix a b assume "(a, b) \<in> r\<^sup>+"
+    then have "f b < f a"
+      by induct (auto intro: * less_trans) }
+  then show ?thesis
+    by (auto intro!: acyclicI)
+qed
+
 lemma acyclic_insert [iff]:
      "acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)"
 apply (simp add: acyclic_def trancl_insert)