proper document source;
authorwenzelm
Mon May 23 12:48:24 2016 +0200 (2016-05-23)
changeset 6310987a4283537e4
parent 63108 02b885591735
child 63110 ccbdce905fca
proper document source;
tuned proofs;
src/HOL/Wellfounded.thy
     1.1 --- a/src/HOL/Wellfounded.thy	Mon May 23 12:18:16 2016 +0200
     1.2 +++ b/src/HOL/Wellfounded.thy	Mon May 23 12:48:24 2016 +0200
     1.3 @@ -317,17 +317,17 @@
     1.4    shows "wf (\<Union>R)"
     1.5    using assms wf_UN[of R "\<lambda>i. i"] by simp
     1.6  
     1.7 -(*Intuition: we find an (R u S)-min element of a nonempty subset A
     1.8 -             by case distinction.
     1.9 -  1. There is a step a -R-> b with a,b : A.
    1.10 -     Pick an R-min element z of the (nonempty) set {a:A | EX b:A. a -R-> b}.
    1.11 -     By definition, there is z':A s.t. z -R-> z'. Because z is R-min in the
    1.12 -     subset, z' must be R-min in A. Because z' has an R-predecessor, it cannot
    1.13 -     have an S-successor and is thus S-min in A as well.
    1.14 -  2. There is no such step.
    1.15 -     Pick an S-min element of A. In this case it must be an R-min
    1.16 -     element of A as well.
    1.17 -*)
    1.18 +text \<open>
    1.19 +  Intuition: We find an \<open>R \<union> S\<close>-min element of a nonempty subset \<open>A\<close> by case distinction.
    1.20 +  \<^enum> There is a step \<open>a \<midarrow>R\<rightarrow> b\<close> with \<open>a, b \<in> A\<close>.
    1.21 +    Pick an \<open>R\<close>-min element \<open>z\<close> of the (nonempty) set \<open>{a\<in>A | \<exists>b\<in>A. a \<midarrow>R\<rightarrow> b}\<close>.
    1.22 +    By definition, there is \<open>z' \<in> A\<close> s.t. \<open>z \<midarrow>R\<rightarrow> z'\<close>. Because \<open>z\<close> is \<open>R\<close>-min in the
    1.23 +    subset, \<open>z'\<close> must be \<open>R\<close>-min in \<open>A\<close>. Because \<open>z'\<close> has an \<open>R\<close>-predecessor, it cannot
    1.24 +    have an \<open>S\<close>-successor and is thus \<open>S\<close>-min in \<open>A\<close> as well.
    1.25 +  \<^enum> There is no such step.
    1.26 +    Pick an \<open>S\<close>-min element of \<open>A\<close>. In this case it must be an \<open>R\<close>-min
    1.27 +    element of \<open>A\<close> as well.
    1.28 +\<close>
    1.29  lemma wf_Un: "wf r \<Longrightarrow> wf s \<Longrightarrow> Domain r \<inter> Range s = {} \<Longrightarrow> wf (r \<union> s)"
    1.30    using wf_union_compatible[of s r]
    1.31    by (auto simp: Un_ac)
    1.32 @@ -342,24 +342,20 @@
    1.33    ultimately show "wf ?B" by (rule wf_subset)
    1.34  next
    1.35    assume "wf ?B"
    1.36 -
    1.37    show "wf ?A"
    1.38    proof (rule wfI_min)
    1.39      fix Q :: "'a set" and x
    1.40      assume "x \<in> Q"
    1.41 -
    1.42 -    with \<open>wf ?B\<close>
    1.43 -    obtain z where "z \<in> Q" and "\<And>y. (y, z) \<in> ?B \<Longrightarrow> y \<notin> Q"
    1.44 +    with \<open>wf ?B\<close> obtain z where "z \<in> Q" and "\<And>y. (y, z) \<in> ?B \<Longrightarrow> y \<notin> Q"
    1.45        by (erule wfE_min)
    1.46 -    then have A1: "\<And>y. (y, z) \<in> R O R \<Longrightarrow> y \<notin> Q"
    1.47 -      and A2: "\<And>y. (y, z) \<in> S O R \<Longrightarrow> y \<notin> Q"
    1.48 -      and A3: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> Q"
    1.49 +    then have 1: "\<And>y. (y, z) \<in> R O R \<Longrightarrow> y \<notin> Q"
    1.50 +      and 2: "\<And>y. (y, z) \<in> S O R \<Longrightarrow> y \<notin> Q"
    1.51 +      and 3: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> Q"
    1.52        by auto
    1.53 -
    1.54      show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> ?A \<longrightarrow> y \<notin> Q"
    1.55      proof (cases "\<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q")
    1.56        case True
    1.57 -      with \<open>z \<in> Q\<close> A3 show ?thesis by blast
    1.58 +      with \<open>z \<in> Q\<close> 3 show ?thesis by blast
    1.59      next
    1.60        case False
    1.61        then obtain z' where "z'\<in>Q" "(z', z) \<in> R" by blast
    1.62 @@ -370,11 +366,11 @@
    1.63          proof
    1.64            assume "(y, z') \<in> R"
    1.65            then have "(y, z) \<in> R O R" using \<open>(z', z) \<in> R\<close> ..
    1.66 -          with A1 show "y \<notin> Q" .
    1.67 +          with 1 show "y \<notin> Q" .
    1.68          next
    1.69            assume "(y, z') \<in> S"
    1.70            then have "(y, z) \<in> S O R" using  \<open>(z', z) \<in> R\<close> ..
    1.71 -          with A2 show "y \<notin> Q" .
    1.72 +          with 2 show "y \<notin> Q" .
    1.73          qed
    1.74        qed
    1.75        with \<open>z' \<in> Q\<close> show ?thesis ..
    1.76 @@ -392,40 +388,55 @@
    1.77  
    1.78  lemma qc_wf_relto_iff:
    1.79    assumes "R O S \<subseteq> (R \<union> S)\<^sup>* O R" \<comment> \<open>R quasi-commutes over S\<close>
    1.80 -  shows "wf (S\<^sup>* O R O S\<^sup>*) \<longleftrightarrow> wf R" (is "wf ?S \<longleftrightarrow> _")
    1.81 +  shows "wf (S\<^sup>* O R O S\<^sup>*) \<longleftrightarrow> wf R"
    1.82 +  (is "wf ?S \<longleftrightarrow> _")
    1.83  proof
    1.84 -  assume "wf ?S"
    1.85 -  moreover have "R \<subseteq> ?S" by auto
    1.86 -  ultimately show "wf R" using wf_subset by auto
    1.87 +  show "wf R" if "wf ?S"
    1.88 +  proof -
    1.89 +    have "R \<subseteq> ?S" by auto
    1.90 +    with that show "wf R" using wf_subset by auto
    1.91 +  qed
    1.92  next
    1.93 -  assume "wf R"
    1.94 -  show "wf ?S"
    1.95 +  show "wf ?S" if "wf R"
    1.96    proof (rule wfI_pf)
    1.97 -    fix A assume A: "A \<subseteq> ?S `` A"
    1.98 +    fix A
    1.99 +    assume A: "A \<subseteq> ?S `` A"
   1.100      let ?X = "(R \<union> S)\<^sup>* `` A"
   1.101      have *: "R O (R \<union> S)\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R"
   1.102 -      proof -
   1.103 -        { fix x y z assume "(y, z) \<in> (R \<union> S)\<^sup>*" and "(x, y) \<in> R"
   1.104 -          then have "(x, z) \<in> (R \<union> S)\<^sup>* O R"
   1.105 -          proof (induct y z)
   1.106 -            case rtrancl_refl then show ?case by auto
   1.107 -          next
   1.108 -            case (rtrancl_into_rtrancl a b c)
   1.109 -            then have "(x, c) \<in> ((R \<union> S)\<^sup>* O (R \<union> S)\<^sup>*) O R" using assms by blast
   1.110 -            then show ?case by simp
   1.111 -          qed }
   1.112 -        then show ?thesis by auto
   1.113 +    proof -
   1.114 +      have "(x, z) \<in> (R \<union> S)\<^sup>* O R" if "(y, z) \<in> (R \<union> S)\<^sup>*" and "(x, y) \<in> R" for x y z
   1.115 +        using that
   1.116 +      proof (induct y z)
   1.117 +        case rtrancl_refl
   1.118 +        then show ?case by auto
   1.119 +      next
   1.120 +        case (rtrancl_into_rtrancl a b c)
   1.121 +        then have "(x, c) \<in> ((R \<union> S)\<^sup>* O (R \<union> S)\<^sup>*) O R"
   1.122 +          using assms by blast
   1.123 +        then show ?case by simp
   1.124        qed
   1.125 -    then have "R O S\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R" using rtrancl_Un_subset by blast
   1.126 -    then have "?S \<subseteq> (R \<union> S)\<^sup>* O (R \<union> S)\<^sup>* O R" by (simp add: relcomp_mono rtrancl_mono)
   1.127 -    also have "\<dots> = (R \<union> S)\<^sup>* O R" by (simp add: O_assoc[symmetric])
   1.128 -    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.129 -    also have "\<dots> \<subseteq> (R \<union> S)\<^sup>* O (R \<union> S)\<^sup>* O R" using * by (simp add: relcomp_mono)
   1.130 -    finally have "?S O (R \<union> S)\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R" by (simp add: O_assoc[symmetric])
   1.131 -    then have "(?S O (R \<union> S)\<^sup>*) `` A \<subseteq> ((R \<union> S)\<^sup>* O R) `` A" by (simp add: Image_mono)
   1.132 -    moreover have "?X \<subseteq> (?S O (R \<union> S)\<^sup>*) `` A" using A by (auto simp: relcomp_Image)
   1.133 -    ultimately have "?X \<subseteq> R `` ?X" by (auto simp: relcomp_Image)
   1.134 -    then have "?X = {}" using \<open>wf R\<close> by (simp add: wfE_pf)
   1.135 +      then show ?thesis by auto
   1.136 +    qed
   1.137 +    then have "R O S\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R"
   1.138 +      using rtrancl_Un_subset by blast
   1.139 +    then have "?S \<subseteq> (R \<union> S)\<^sup>* O (R \<union> S)\<^sup>* O R"
   1.140 +      by (simp add: relcomp_mono rtrancl_mono)
   1.141 +    also have "\<dots> = (R \<union> S)\<^sup>* O R"
   1.142 +      by (simp add: O_assoc[symmetric])
   1.143 +    finally have "?S O (R \<union> S)\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R O (R \<union> S)\<^sup>*"
   1.144 +      by (simp add: O_assoc[symmetric] relcomp_mono)
   1.145 +    also have "\<dots> \<subseteq> (R \<union> S)\<^sup>* O (R \<union> S)\<^sup>* O R"
   1.146 +      using * by (simp add: relcomp_mono)
   1.147 +    finally have "?S O (R \<union> S)\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R"
   1.148 +      by (simp add: O_assoc[symmetric])
   1.149 +    then have "(?S O (R \<union> S)\<^sup>*) `` A \<subseteq> ((R \<union> S)\<^sup>* O R) `` A"
   1.150 +      by (simp add: Image_mono)
   1.151 +    moreover have "?X \<subseteq> (?S O (R \<union> S)\<^sup>*) `` A"
   1.152 +      using A by (auto simp: relcomp_Image)
   1.153 +    ultimately have "?X \<subseteq> R `` ?X"
   1.154 +      by (auto simp: relcomp_Image)
   1.155 +    then have "?X = {}"
   1.156 +      using \<open>wf R\<close> by (simp add: wfE_pf)
   1.157      moreover have "A \<subseteq> ?X" by auto
   1.158      ultimately show "A = {}" by simp
   1.159    qed
   1.160 @@ -664,25 +675,15 @@
   1.161  text \<open>Set versions of the above theorems\<close>
   1.162  
   1.163  lemmas acc_induct = accp_induct [to_set]
   1.164 -
   1.165  lemmas acc_induct_rule = acc_induct [rule_format, induct set: acc]
   1.166 -
   1.167  lemmas acc_downward = accp_downward [to_set]
   1.168 -
   1.169  lemmas not_acc_down = not_accp_down [to_set]
   1.170 -
   1.171  lemmas acc_downwards_aux = accp_downwards_aux [to_set]
   1.172 -
   1.173  lemmas acc_downwards = accp_downwards [to_set]
   1.174 -
   1.175  lemmas acc_wfI = accp_wfPI [to_set]
   1.176 -
   1.177  lemmas acc_wfD = accp_wfPD [to_set]
   1.178 -
   1.179  lemmas wf_acc_iff = wfP_accp_iff [to_set]
   1.180 -
   1.181  lemmas acc_subset = accp_subset [to_set]
   1.182 -
   1.183  lemmas acc_subset_induct = accp_subset_induct [to_set]
   1.184  
   1.185  
   1.186 @@ -691,7 +692,7 @@
   1.187  text \<open>Inverse Image\<close>
   1.188  
   1.189  lemma wf_inv_image [simp,intro!]: "wf r \<Longrightarrow> wf (inv_image r f)" for f :: "'a \<Rightarrow> 'b"
   1.190 -apply (simp (no_asm_use) add: inv_image_def wf_eq_minimal)
   1.191 +apply (simp add: inv_image_def wf_eq_minimal)
   1.192  apply clarify
   1.193  apply (subgoal_tac "\<exists>w::'b. w \<in> {w. \<exists>x::'a. x \<in> Q \<and> f x = w}")
   1.194  prefer 2 apply (blast del: allE)
   1.195 @@ -731,7 +732,7 @@
   1.196  lemma wf_lex_prod [intro!]: "wf ra \<Longrightarrow> wf rb \<Longrightarrow> wf (ra <*lex*> rb)"
   1.197  apply (unfold wf_def lex_prod_def)
   1.198  apply (rule allI, rule impI)
   1.199 -apply (simp (no_asm_use) only: split_paired_All)
   1.200 +apply (simp only: split_paired_All)
   1.201  apply (drule spec, erule mp)
   1.202  apply (rule allI, rule impI)
   1.203  apply (drule spec, erule mp, blast)