New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
authorpaulson <lp15@cam.ac.uk>
Wed Jun 17 14:35:50 2015 +0100 (2015-06-17)
changeset 60493866f41a869e6
parent 60492 db0f4f4c17c7
child 60494 e726f88232d3
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
src/HOL/Wellfounded.thy
     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 *}