merged
authornipkow
Wed, 17 Jun 2015 17:21:20 +0200
changeset 60496 12f58a22eb11
parent 60494 e726f88232d3 (diff)
parent 60495 d7ff0a1df90a (current diff)
child 60497 010c26e24c72
merged
--- a/src/HOL/Groups_Big.thy	Wed Jun 17 17:21:11 2015 +0200
+++ b/src/HOL/Groups_Big.thy	Wed Jun 17 17:21:20 2015 +0200
@@ -490,11 +490,11 @@
 written @{text"\<Sum>x\<in>A. e"}. *}
 
 syntax
-  "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_. _)" [0, 51, 10] 10)
+  "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_./ _)" [0, 51, 10] 10)
 syntax (xsymbols)
-  "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
+  "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(2\<Sum>_\<in>_./ _)" [0, 51, 10] 10)
 syntax (HTML output)
-  "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
+  "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(2\<Sum>_\<in>_./ _)" [0, 51, 10] 10)
 
 translations -- {* Beware of argument permutation! *}
   "SUM i:A. b" == "CONST setsum (%i. b) A"
@@ -506,9 +506,9 @@
 syntax
   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
 syntax (xsymbols)
-  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
+  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Sum>_ | (_)./ _)" [0,0,10] 10)
 syntax (HTML output)
-  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
+  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Sum>_ | (_)./ _)" [0,0,10] 10)
 
 translations
   "SUM x|P. t" => "CONST setsum (%x. t) {x. P}"
@@ -1054,11 +1054,11 @@
 end
 
 syntax
-  "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3PROD _:_. _)" [0, 51, 10] 10)
+  "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(4PROD _:_./ _)" [0, 51, 10] 10)
 syntax (xsymbols)
-  "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
+  "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(2\<Prod>_\<in>_./ _)" [0, 51, 10] 10)
 syntax (HTML output)
-  "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
+  "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(2\<Prod>_\<in>_./ _)" [0, 51, 10] 10)
 
 translations -- {* Beware of argument permutation! *}
   "PROD i:A. b" == "CONST setprod (%i. b) A" 
@@ -1068,11 +1068,11 @@
  @{text"\<Prod>x|P. e"}. *}
 
 syntax
-  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3PROD _ |/ _./ _)" [0,0,10] 10)
+  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(4PROD _ |/ _./ _)" [0,0,10] 10)
 syntax (xsymbols)
-  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
+  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Prod>_ | (_)./ _)" [0,0,10] 10)
 syntax (HTML output)
-  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
+  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Prod>_ | (_)./ _)" [0,0,10] 10)
 
 translations
   "PROD x|P. t" => "CONST setprod (%x. t) {x. P}"
--- a/src/HOL/Wellfounded.thy	Wed Jun 17 17:21:11 2015 +0200
+++ b/src/HOL/Wellfounded.thy	Wed Jun 17 17:21:20 2015 +0200
@@ -318,7 +318,6 @@
   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.
-
 *)
 lemma wf_Un:
      "[| wf r; wf s; Domain r Int Range s = {} |] ==> wf(r Un s)"
@@ -382,30 +381,59 @@
 
 subsection {* Well-Foundedness of Composition *}
 
-text{* Provided by Tjark Weber: *}
+text \<open>Bachmair and Dershowitz 1986, Lemma 2. [Provided by Tjark Weber]\<close>
 
-lemma wf_relcomp_compatible:
+lemma qc_wf_relto_iff:
+  assumes "R O S \<subseteq> (R \<union> S)\<^sup>* O R" -- \<open>R quasi-commutes over S\<close>
+  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
+next
+  assume "wf R"
+  show "wf ?S"
+  proof (rule wfI_pf)
+    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
+      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
+qed
+
+corollary wf_relcomp_compatible:
   assumes "wf R" and "R O S \<subseteq> S O R"
   shows "wf (S O R)"
-proof (rule wfI_pf)
-  fix A assume A: "A \<subseteq> (S O R) `` A"
-  {
-    fix n have "(S ^^ n) `` A \<subseteq> R `` (S ^^ Suc n) `` A"
-    proof (induction n)
-      case 0 show ?case using A by (simp add: relcomp_Image)
-    next
-      case (Suc n)
-      then have "S `` (S ^^ n) `` A \<subseteq> S `` R `` (S ^^ Suc n) `` A"
-        by (simp add: Image_mono)
-      also have "\<dots> \<subseteq> R `` S `` (S ^^ Suc n) `` A" using assms(2)
-        by (simp add: Image_mono O_assoc relcomp_Image[symmetric] relcomp_mono)
-      finally show ?case by (simp add: relcomp_Image)
-    qed
-  }
-  then have "(\<Union>n. (S ^^ n) `` A) \<subseteq> R `` (\<Union>n. (S ^^ n) `` A)" by blast
-  then have "(\<Union>n. (S ^^ n) `` A) = {}"
-    using assms(1) by (simp only: wfE_pf)
-  then show "A = {}" using relpow.simps(1) by blast
+proof -
+  have "R O S \<subseteq> (R \<union> S)\<^sup>* O R"
+    using assms by blast
+  then have "wf (S\<^sup>* O R O S\<^sup>*)"
+    by (simp add: assms qc_wf_relto_iff)
+  then show ?thesis
+    by (rule Wellfounded.wf_subset) blast
 qed
 
 
@@ -486,7 +514,7 @@
   by (simp add: less_than_def less_eq)
 
 lemma wf_less: "wf {(x, y::nat). x < y}"
-  using wf_less_than by (simp add: less_than_def less_eq [symmetric])
+  by (rule Wellfounded.wellorder_class.wf)
 
 
 subsection {* Accessible Part *}