summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Mon, 23 May 2016 12:48:24 +0200 | |

changeset 63109 | 87a4283537e4 |

parent 63108 | 02b885591735 |

child 63110 | ccbdce905fca |

proper document source;
tuned proofs;

--- a/src/HOL/Wellfounded.thy Mon May 23 12:18:16 2016 +0200 +++ b/src/HOL/Wellfounded.thy Mon May 23 12:48:24 2016 +0200 @@ -317,17 +317,17 @@ shows "wf (\<Union>R)" using assms wf_UN[of R "\<lambda>i. i"] by simp -(*Intuition: we find an (R u S)-min element of a nonempty subset A - by case distinction. - 1. There is a step a -R-> b with a,b : A. - Pick an R-min element z of the (nonempty) set {a:A | EX b:A. a -R-> b}. - By definition, there is z':A s.t. z -R-> z'. Because z is R-min in the - subset, z' must be R-min in A. Because z' has an R-predecessor, it cannot - have an S-successor and is thus S-min in A as well. - 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. -*) +text \<open> + Intuition: We find an \<open>R \<union> S\<close>-min element of a nonempty subset \<open>A\<close> by case distinction. + \<^enum> There is a step \<open>a \<midarrow>R\<rightarrow> b\<close> with \<open>a, b \<in> A\<close>. + 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>. + 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 + 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 + have an \<open>S\<close>-successor and is thus \<open>S\<close>-min in \<open>A\<close> as well. + \<^enum> There is no such step. + Pick an \<open>S\<close>-min element of \<open>A\<close>. In this case it must be an \<open>R\<close>-min + element of \<open>A\<close> as well. +\<close> lemma wf_Un: "wf r \<Longrightarrow> wf s \<Longrightarrow> Domain r \<inter> Range s = {} \<Longrightarrow> wf (r \<union> s)" using wf_union_compatible[of s r] by (auto simp: Un_ac) @@ -342,24 +342,20 @@ ultimately show "wf ?B" by (rule wf_subset) next assume "wf ?B" - show "wf ?A" proof (rule wfI_min) fix Q :: "'a set" and x assume "x \<in> Q" - - with \<open>wf ?B\<close> - obtain z where "z \<in> Q" and "\<And>y. (y, z) \<in> ?B \<Longrightarrow> y \<notin> Q" + with \<open>wf ?B\<close> obtain z where "z \<in> Q" and "\<And>y. (y, z) \<in> ?B \<Longrightarrow> y \<notin> Q" by (erule wfE_min) - then have A1: "\<And>y. (y, z) \<in> R O R \<Longrightarrow> y \<notin> Q" - and A2: "\<And>y. (y, z) \<in> S O R \<Longrightarrow> y \<notin> Q" - and A3: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> Q" + then have 1: "\<And>y. (y, z) \<in> R O R \<Longrightarrow> y \<notin> Q" + and 2: "\<And>y. (y, z) \<in> S O R \<Longrightarrow> y \<notin> Q" + and 3: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> Q" by auto - show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> ?A \<longrightarrow> y \<notin> Q" proof (cases "\<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q") case True - with \<open>z \<in> Q\<close> A3 show ?thesis by blast + with \<open>z \<in> Q\<close> 3 show ?thesis by blast next case False then obtain z' where "z'\<in>Q" "(z', z) \<in> R" by blast @@ -370,11 +366,11 @@ proof assume "(y, z') \<in> R" then have "(y, z) \<in> R O R" using \<open>(z', z) \<in> R\<close> .. - with A1 show "y \<notin> Q" . + with 1 show "y \<notin> Q" . next assume "(y, z') \<in> S" then have "(y, z) \<in> S O R" using \<open>(z', z) \<in> R\<close> .. - with A2 show "y \<notin> Q" . + with 2 show "y \<notin> Q" . qed qed with \<open>z' \<in> Q\<close> show ?thesis .. @@ -392,40 +388,55 @@ lemma qc_wf_relto_iff: assumes "R O S \<subseteq> (R \<union> S)\<^sup>* O R" \<comment> \<open>R quasi-commutes over S\<close> - shows "wf (S\<^sup>* O R O S\<^sup>*) \<longleftrightarrow> wf R" (is "wf ?S \<longleftrightarrow> _") + 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 + show "wf R" if "wf ?S" + proof - + have "R \<subseteq> ?S" by auto + with that show "wf R" using wf_subset by auto + qed next - assume "wf R" - show "wf ?S" + show "wf ?S" if "wf R" proof (rule wfI_pf) - fix A assume A: "A \<subseteq> ?S `` A" + 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 + proof - + 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 + using that + 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 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) + 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 @@ -664,25 +675,15 @@ text \<open>Set versions of the above theorems\<close> lemmas acc_induct = accp_induct [to_set] - lemmas acc_induct_rule = acc_induct [rule_format, induct set: acc] - lemmas acc_downward = accp_downward [to_set] - lemmas not_acc_down = not_accp_down [to_set] - lemmas acc_downwards_aux = accp_downwards_aux [to_set] - lemmas acc_downwards = accp_downwards [to_set] - lemmas acc_wfI = accp_wfPI [to_set] - lemmas acc_wfD = accp_wfPD [to_set] - lemmas wf_acc_iff = wfP_accp_iff [to_set] - lemmas acc_subset = accp_subset [to_set] - lemmas acc_subset_induct = accp_subset_induct [to_set] @@ -691,7 +692,7 @@ text \<open>Inverse Image\<close> lemma wf_inv_image [simp,intro!]: "wf r \<Longrightarrow> wf (inv_image r f)" for f :: "'a \<Rightarrow> 'b" -apply (simp (no_asm_use) add: inv_image_def wf_eq_minimal) +apply (simp add: inv_image_def wf_eq_minimal) apply clarify apply (subgoal_tac "\<exists>w::'b. w \<in> {w. \<exists>x::'a. x \<in> Q \<and> f x = w}") prefer 2 apply (blast del: allE) @@ -731,7 +732,7 @@ lemma wf_lex_prod [intro!]: "wf ra \<Longrightarrow> wf rb \<Longrightarrow> wf (ra <*lex*> rb)" apply (unfold wf_def lex_prod_def) apply (rule allI, rule impI) -apply (simp (no_asm_use) only: split_paired_All) +apply (simp only: split_paired_All) apply (drule spec, erule mp) apply (rule allI, rule impI) apply (drule spec, erule mp, blast)