--- 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 *}