# HG changeset patch
# User wenzelm
# Date 1464000504 -7200
# Node ID 87a4283537e408e58d80f30b2ca324e4ba90e54b
# Parent  02b8855917358ff9dda70cc8896f0c6ceda999af
proper document source;
tuned proofs;

diff -r 02b885591735 -r 87a4283537e4 src/HOL/Wellfounded.thy
--- 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)