src/HOL/Wellfounded.thy
changeset 60148 f0fc2378a479
parent 59807 22bc39064290
child 60493 866f41a869e6
     1.1 --- a/src/HOL/Wellfounded.thy	Sat Apr 25 17:38:22 2015 +0200
     1.2 +++ b/src/HOL/Wellfounded.thy	Mon Apr 27 15:02:51 2015 +0200
     1.3 @@ -380,6 +380,35 @@
     1.4    by (rule wf_union_merge [where S = "{}", simplified])
     1.5  
     1.6  
     1.7 +subsection {* Well-Foundedness of Composition *}
     1.8 +
     1.9 +text{* Provided by Tjark Weber: *}
    1.10 +
    1.11 +lemma wf_relcomp_compatible:
    1.12 +  assumes "wf R" and "R O S \<subseteq> S O R"
    1.13 +  shows "wf (S O R)"
    1.14 +proof (rule wfI_pf)
    1.15 +  fix A assume A: "A \<subseteq> (S O R) `` A"
    1.16 +  {
    1.17 +    fix n have "(S ^^ n) `` A \<subseteq> R `` (S ^^ Suc n) `` A"
    1.18 +    proof (induction n)
    1.19 +      case 0 show ?case using A by (simp add: relcomp_Image)
    1.20 +    next
    1.21 +      case (Suc n)
    1.22 +      then have "S `` (S ^^ n) `` A \<subseteq> S `` R `` (S ^^ Suc n) `` A"
    1.23 +        by (simp add: Image_mono)
    1.24 +      also have "\<dots> \<subseteq> R `` S `` (S ^^ Suc n) `` A" using assms(2)
    1.25 +        by (simp add: Image_mono O_assoc relcomp_Image[symmetric] relcomp_mono)
    1.26 +      finally show ?case by (simp add: relcomp_Image)
    1.27 +    qed
    1.28 +  }
    1.29 +  then have "(\<Union>n. (S ^^ n) `` A) \<subseteq> R `` (\<Union>n. (S ^^ n) `` A)" by blast
    1.30 +  then have "(\<Union>n. (S ^^ n) `` A) = {}"
    1.31 +    using assms(1) by (simp only: wfE_pf)
    1.32 +  then show "A = {}" using relpow.simps(1) by blast
    1.33 +qed
    1.34 +
    1.35 +
    1.36  subsection {* Acyclic relations *}
    1.37  
    1.38  lemma wf_acyclic: "wf r ==> acyclic r"