src/HOL/Wellfounded.thy
 changeset 60493 866f41a869e6 parent 60148 f0fc2378a479 child 60758 d8d85a8172b5
```     1.1 --- a/src/HOL/Wellfounded.thy	Tue Jun 16 20:50:00 2015 +0100
1.2 +++ b/src/HOL/Wellfounded.thy	Wed Jun 17 14:35:50 2015 +0100
1.3 @@ -318,7 +318,6 @@
1.4    2. There is no such step.
1.5       Pick an S-min element of A. In this case it must be an R-min
1.6       element of A as well.
1.7 -
1.8  *)
1.9  lemma wf_Un:
1.10       "[| wf r; wf s; Domain r Int Range s = {} |] ==> wf(r Un s)"
1.11 @@ -382,30 +381,59 @@
1.12
1.13  subsection {* Well-Foundedness of Composition *}
1.14
1.15 -text{* Provided by Tjark Weber: *}
1.16 +text \<open>Bachmair and Dershowitz 1986, Lemma 2. [Provided by Tjark Weber]\<close>
1.17
1.18 -lemma wf_relcomp_compatible:
1.19 +lemma qc_wf_relto_iff:
1.20 +  assumes "R O S \<subseteq> (R \<union> S)\<^sup>* O R" -- \<open>R quasi-commutes over S\<close>
1.21 +  shows "wf (S\<^sup>* O R O S\<^sup>*) \<longleftrightarrow> wf R" (is "wf ?S \<longleftrightarrow> _")
1.22 +proof
1.23 +  assume "wf ?S"
1.24 +  moreover have "R \<subseteq> ?S" by auto
1.25 +  ultimately show "wf R" using wf_subset by auto
1.26 +next
1.27 +  assume "wf R"
1.28 +  show "wf ?S"
1.29 +  proof (rule wfI_pf)
1.30 +    fix A assume A: "A \<subseteq> ?S `` A"
1.31 +    let ?X = "(R \<union> S)\<^sup>* `` A"
1.32 +    have *: "R O (R \<union> S)\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R"
1.33 +      proof -
1.34 +        { fix x y z assume "(y, z) \<in> (R \<union> S)\<^sup>*" and "(x, y) \<in> R"
1.35 +          then have "(x, z) \<in> (R \<union> S)\<^sup>* O R"
1.36 +          proof (induct y z)
1.37 +            case rtrancl_refl then show ?case by auto
1.38 +          next
1.39 +            case (rtrancl_into_rtrancl a b c)
1.40 +            then have "(x, c) \<in> ((R \<union> S)\<^sup>* O (R \<union> S)\<^sup>*) O R" using assms by blast
1.41 +            then show ?case by simp
1.42 +          qed }
1.43 +        then show ?thesis by auto
1.44 +      qed
1.45 +    then have "R O S\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R" using rtrancl_Un_subset by blast
1.46 +    then have "?S \<subseteq> (R \<union> S)\<^sup>* O (R \<union> S)\<^sup>* O R" by (simp add: relcomp_mono rtrancl_mono)
1.47 +    also have "\<dots> = (R \<union> S)\<^sup>* O R" by (simp add: O_assoc[symmetric])
1.48 +    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)
1.49 +    also have "\<dots> \<subseteq> (R \<union> S)\<^sup>* O (R \<union> S)\<^sup>* O R" using * by (simp add: relcomp_mono)
1.50 +    finally have "?S O (R \<union> S)\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R" by (simp add: O_assoc[symmetric])
1.51 +    then have "(?S O (R \<union> S)\<^sup>*) `` A \<subseteq> ((R \<union> S)\<^sup>* O R) `` A" by (simp add: Image_mono)
1.52 +    moreover have "?X \<subseteq> (?S O (R \<union> S)\<^sup>*) `` A" using A by (auto simp: relcomp_Image)
1.53 +    ultimately have "?X \<subseteq> R `` ?X" by (auto simp: relcomp_Image)
1.54 +    then have "?X = {}" using \<open>wf R\<close> by (simp add: wfE_pf)
1.55 +    moreover have "A \<subseteq> ?X" by auto
1.56 +    ultimately show "A = {}" by simp
1.57 +  qed
1.58 +qed
1.59 +
1.60 +corollary wf_relcomp_compatible:
1.61    assumes "wf R" and "R O S \<subseteq> S O R"
1.62    shows "wf (S O R)"
1.63 -proof (rule wfI_pf)
1.64 -  fix A assume A: "A \<subseteq> (S O R) `` A"
1.65 -  {
1.66 -    fix n have "(S ^^ n) `` A \<subseteq> R `` (S ^^ Suc n) `` A"
1.67 -    proof (induction n)
1.68 -      case 0 show ?case using A by (simp add: relcomp_Image)
1.69 -    next
1.70 -      case (Suc n)
1.71 -      then have "S `` (S ^^ n) `` A \<subseteq> S `` R `` (S ^^ Suc n) `` A"
1.72 -        by (simp add: Image_mono)
1.73 -      also have "\<dots> \<subseteq> R `` S `` (S ^^ Suc n) `` A" using assms(2)
1.74 -        by (simp add: Image_mono O_assoc relcomp_Image[symmetric] relcomp_mono)
1.75 -      finally show ?case by (simp add: relcomp_Image)
1.76 -    qed
1.77 -  }
1.78 -  then have "(\<Union>n. (S ^^ n) `` A) \<subseteq> R `` (\<Union>n. (S ^^ n) `` A)" by blast
1.79 -  then have "(\<Union>n. (S ^^ n) `` A) = {}"
1.80 -    using assms(1) by (simp only: wfE_pf)
1.81 -  then show "A = {}" using relpow.simps(1) by blast
1.82 +proof -
1.83 +  have "R O S \<subseteq> (R \<union> S)\<^sup>* O R"
1.84 +    using assms by blast
1.85 +  then have "wf (S\<^sup>* O R O S\<^sup>*)"
1.86 +    by (simp add: assms qc_wf_relto_iff)
1.87 +  then show ?thesis
1.88 +    by (rule Wellfounded.wf_subset) blast
1.89  qed
1.90
1.91
1.92 @@ -486,7 +514,7 @@
1.93    by (simp add: less_than_def less_eq)
1.94
1.95  lemma wf_less: "wf {(x, y::nat). x < y}"
1.96 -  using wf_less_than by (simp add: less_than_def less_eq [symmetric])
1.97 +  by (rule Wellfounded.wellorder_class.wf)
1.98
1.99
1.100  subsection {* Accessible Part *}
```