author wenzelm Mon May 23 12:48:24 2016 +0200 (2016-05-23) changeset 63109 87a4283537e4 parent 63108 02b885591735 child 63110 ccbdce905fca
proper document source;
tuned proofs;
 src/HOL/Wellfounded.thy file | annotate | diff | revisions
```     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)
```