# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1434548150 -3600
# Node ID 866f41a869e6381ee201dcffeca2cf71018b4331
# Parent  db0f4f4c17c732cbf43bbc7fcd09b997a0a60ea2
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.

diff -r db0f4f4c17c7 -r 866f41a869e6 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Tue Jun 16 20:50:00 2015 +0100
+++ b/src/HOL/Wellfounded.thy	Wed Jun 17 14:35:50 2015 +0100
@@ -318,7 +318,6 @@
   2. There is no such step.
      Pick an S-min element of A. In this case it must be an R-min
      element of A as well.
-
 *)
 lemma wf_Un:
      "[| wf r; wf s; Domain r Int Range s = {} |] ==> wf(r Un s)"
@@ -382,30 +381,59 @@
 
 subsection {* Well-Foundedness of Composition *}
 
-text{* Provided by Tjark Weber: *}
+text \<open>Bachmair and Dershowitz 1986, Lemma 2. [Provided by Tjark Weber]\<close>
 
-lemma wf_relcomp_compatible:
+lemma qc_wf_relto_iff:
+  assumes "R O S \<subseteq> (R \<union> S)\<^sup>* O R" -- \<open>R quasi-commutes over S\<close>
+  shows "wf (S\<^sup>* O R O S\<^sup>*) \<longleftrightarrow> wf R" (is "wf ?S \<longleftrightarrow> _")
+proof
+  assume "wf ?S"
+  moreover have "R \<subseteq> ?S" by auto
+  ultimately show "wf R" using wf_subset by auto
+next
+  assume "wf R"
+  show "wf ?S"
+  proof (rule wfI_pf)
+    fix A assume A: "A \<subseteq> ?S `` A"
+    let ?X = "(R \<union> S)\<^sup>* `` A"
+    have *: "R O (R \<union> S)\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R"
+      proof -
+        { fix x y z assume "(y, z) \<in> (R \<union> S)\<^sup>*" and "(x, y) \<in> R"
+          then have "(x, z) \<in> (R \<union> S)\<^sup>* O R"
+          proof (induct y z)
+            case rtrancl_refl then show ?case by auto
+          next
+            case (rtrancl_into_rtrancl a b c)
+            then have "(x, c) \<in> ((R \<union> S)\<^sup>* O (R \<union> S)\<^sup>*) O R" using assms by blast
+            then show ?case by simp
+          qed }
+        then show ?thesis by auto
+      qed
+    then have "R O S\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R" using rtrancl_Un_subset by blast
+    then have "?S \<subseteq> (R \<union> S)\<^sup>* O (R \<union> S)\<^sup>* O R" by (simp add: relcomp_mono rtrancl_mono)
+    also have "\<dots> = (R \<union> S)\<^sup>* O R" by (simp add: O_assoc[symmetric])
+    finally have "?S O (R \<union> S)\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R O (R \<union> S)\<^sup>*" by (simp add: O_assoc[symmetric] relcomp_mono)
+    also have "\<dots> \<subseteq> (R \<union> S)\<^sup>* O (R \<union> S)\<^sup>* O R" using * by (simp add: relcomp_mono)
+    finally have "?S O (R \<union> S)\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R" by (simp add: O_assoc[symmetric])
+    then have "(?S O (R \<union> S)\<^sup>*) `` A \<subseteq> ((R \<union> S)\<^sup>* O R) `` A" by (simp add: Image_mono)
+    moreover have "?X \<subseteq> (?S O (R \<union> S)\<^sup>*) `` A" using A by (auto simp: relcomp_Image)
+    ultimately have "?X \<subseteq> R `` ?X" by (auto simp: relcomp_Image)
+    then have "?X = {}" using \<open>wf R\<close> by (simp add: wfE_pf)
+    moreover have "A \<subseteq> ?X" by auto
+    ultimately show "A = {}" by simp
+  qed
+qed
+
+corollary 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
+proof -
+  have "R O S \<subseteq> (R \<union> S)\<^sup>* O R"
+    using assms by blast
+  then have "wf (S\<^sup>* O R O S\<^sup>*)"
+    by (simp add: assms qc_wf_relto_iff)
+  then show ?thesis
+    by (rule Wellfounded.wf_subset) blast
 qed
 
 
@@ -486,7 +514,7 @@
   by (simp add: less_than_def less_eq)
 
 lemma wf_less: "wf {(x, y::nat). x < y}"
-  using wf_less_than by (simp add: less_than_def less_eq [symmetric])
+  by (rule Wellfounded.wellorder_class.wf)
 
 
 subsection {* Accessible Part *}