# HG changeset patch
# User nipkow
# Date 1430139771 -7200
# Node ID f0fc2378a479e2d37fcf9cc0b7bc8207716fa0aa
# Parent  6d7b7a037e8d3bca2b9535e660ea6210b7a87e6b
new lemma

diff -r 6d7b7a037e8d -r f0fc2378a479 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Sat Apr 25 17:38:22 2015 +0200
+++ b/src/HOL/Wellfounded.thy	Mon Apr 27 15:02:51 2015 +0200
@@ -380,6 +380,35 @@
   by (rule wf_union_merge [where S = "{}", simplified])
 
 
+subsection {* Well-Foundedness of Composition *}
+
+text{* Provided by Tjark Weber: *}
+
+lemma wf_relcomp_compatible:
+  assumes "wf R" and "R O S \<subseteq> S O R"
+  shows "wf (S O R)"
+proof (rule wfI_pf)
+  fix A assume A: "A \<subseteq> (S O R) `` A"
+  {
+    fix n have "(S ^^ n) `` A \<subseteq> R `` (S ^^ Suc n) `` A"
+    proof (induction n)
+      case 0 show ?case using A by (simp add: relcomp_Image)
+    next
+      case (Suc n)
+      then have "S `` (S ^^ n) `` A \<subseteq> S `` R `` (S ^^ Suc n) `` A"
+        by (simp add: Image_mono)
+      also have "\<dots> \<subseteq> R `` S `` (S ^^ Suc n) `` A" using assms(2)
+        by (simp add: Image_mono O_assoc relcomp_Image[symmetric] relcomp_mono)
+      finally show ?case by (simp add: relcomp_Image)
+    qed
+  }
+  then have "(\<Union>n. (S ^^ n) `` A) \<subseteq> R `` (\<Union>n. (S ^^ n) `` A)" by blast
+  then have "(\<Union>n. (S ^^ n) `` A) = {}"
+    using assms(1) by (simp only: wfE_pf)
+  then show "A = {}" using relpow.simps(1) by blast
+qed
+
+
 subsection {* Acyclic relations *}
 
 lemma wf_acyclic: "wf r ==> acyclic r"