--- a/Admin/PLATFORMS Sat Jan 30 20:47:00 2021 +0100
+++ b/Admin/PLATFORMS Sat Jan 30 21:43:13 2021 +0100
@@ -38,7 +38,7 @@
x86_64-darwin macOS 10.13 High Sierra (lapbroy68 MacBookPro11,2)
macOS 10.14 Mojave (mini2 Macmini8,1)
macOS 10.15 Catalina (laramac01 Macmini8,1)
- macOS 11.1 Big Sur
+ macOS 11.1 Big Sur (mini1 Macmini8,1)
x86_64-windows Windows 10
x86_64-cygwin Cygwin 3.1.x https://isabelle.sketis.net/cygwin_2021 (x86_64/release)
--- a/CONTRIBUTORS Sat Jan 30 20:47:00 2021 +0100
+++ b/CONTRIBUTORS Sat Jan 30 21:43:13 2021 +0100
@@ -3,6 +3,13 @@
listed as an author in one of the source files of this Isabelle distribution.
+Contributions to this Isabelle version
+--------------------------------------
+
+* January 2021: Jakub Kądziołka
+ Some lemmas for HOL-Computational_Algebra.
+
+
Contributions to Isabelle2021
-----------------------------
--- a/src/HOL/Computational_Algebra/Factorial_Ring.thy Sat Jan 30 20:47:00 2021 +0100
+++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy Sat Jan 30 21:43:13 2021 +0100
@@ -898,6 +898,26 @@
ultimately show ?thesis by (rule finite_subset)
qed
+lemma infinite_unit_divisor_powers:
+ assumes "y \<noteq> 0"
+ assumes "is_unit x"
+ shows "infinite {n. x^n dvd y}"
+proof -
+ from `is_unit x` have "is_unit (x^n)" for n
+ using is_unit_power_iff by auto
+ hence "x^n dvd y" for n
+ by auto
+ hence "{n. x^n dvd y} = UNIV"
+ by auto
+ thus ?thesis
+ by auto
+qed
+
+corollary is_unit_iff_infinite_divisor_powers:
+ assumes "y \<noteq> 0"
+ shows "is_unit x \<longleftrightarrow> infinite {n. x^n dvd y}"
+ using infinite_unit_divisor_powers finite_divisor_powers assms by auto
+
lemma prime_elem_iff_irreducible: "prime_elem x \<longleftrightarrow> irreducible x"
by (blast intro: irreducible_imp_prime_elem prime_elem_imp_irreducible)
@@ -1606,8 +1626,8 @@
thus ?thesis by simp
qed
-lemma multiplicity_zero_1 [simp]: "multiplicity 0 x = 0"
- by (metis (mono_tags) local.dvd_0_left multiplicity_zero not_dvd_imp_multiplicity_0)
+lemma multiplicity_zero_left [simp]: "multiplicity 0 x = 0"
+ by (cases "x = 0") (auto intro: not_dvd_imp_multiplicity_0)
lemma inj_on_Prod_primes:
assumes "\<And>P p. P \<in> A \<Longrightarrow> p \<in> P \<Longrightarrow> prime p"
@@ -2129,6 +2149,91 @@
with assms show False by auto
qed
+text \<open>Now a string of results due to Jakub Kądziołka\<close>
+
+lemma multiplicity_dvd_iff_dvd:
+ assumes "x \<noteq> 0"
+ shows "p^k dvd x \<longleftrightarrow> p^k dvd p^multiplicity p x"
+proof (cases "is_unit p")
+ case True
+ then have "is_unit (p^k)"
+ using is_unit_power_iff by simp
+ hence "p^k dvd x"
+ by auto
+ moreover from `is_unit p` have "p^k dvd p^multiplicity p x"
+ using multiplicity_unit_left is_unit_power_iff by simp
+ ultimately show ?thesis by simp
+next
+ case False
+ show ?thesis
+ proof (cases "p = 0")
+ case True
+ then have "p^multiplicity p x = 1"
+ by simp
+ moreover have "p^k dvd x \<Longrightarrow> k = 0"
+ proof (rule ccontr)
+ assume "p^k dvd x" and "k \<noteq> 0"
+ with `p = 0` have "p^k = 0" by auto
+ with `p^k dvd x` have "0 dvd x" by auto
+ hence "x = 0" by auto
+ with `x \<noteq> 0` show False by auto
+ qed
+ ultimately show ?thesis
+ by (auto simp add: is_unit_power_iff `\<not> is_unit p`)
+ next
+ case False
+ with `x \<noteq> 0` `\<not> is_unit p` show ?thesis
+ by (simp add: power_dvd_iff_le_multiplicity dvd_power_iff multiplicity_same_power)
+ qed
+qed
+
+lemma multiplicity_decomposeI:
+ assumes "x = p^k * x'" and "\<not> p dvd x'" and "p \<noteq> 0"
+ shows "multiplicity p x = k"
+ using assms local.multiplicity_eqI local.power_Suc2 by force
+
+lemma multiplicity_sum_lt:
+ assumes "multiplicity p a < multiplicity p b" "a \<noteq> 0" "b \<noteq> 0"
+ shows "multiplicity p (a + b) = multiplicity p a"
+proof -
+ let ?vp = "multiplicity p"
+ have unit: "\<not> is_unit p"
+ proof
+ assume "is_unit p"
+ then have "?vp a = 0" and "?vp b = 0" using multiplicity_unit_left by auto
+ with assms show False by auto
+ qed
+
+ from multiplicity_decompose' obtain a' where a': "a = p^?vp a * a'" "\<not> p dvd a'"
+ using unit assms by metis
+ from multiplicity_decompose' obtain b' where b': "b = p^?vp b * b'"
+ using unit assms by metis
+
+ show "?vp (a + b) = ?vp a"
+ proof (rule multiplicity_decomposeI)
+ let ?k = "?vp b - ?vp a"
+ from assms have k: "?k > 0" by simp
+ with b' have "b = p^?vp a * p^?k * b'"
+ by (simp flip: power_add)
+ with a' show *: "a + b = p^?vp a * (a' + p^?k * b')"
+ by (simp add: ac_simps distrib_left)
+ moreover show "\<not> p dvd a' + p^?k * b'"
+ using a' k dvd_add_left_iff by auto
+ show "p \<noteq> 0" using assms by auto
+ qed
+qed
+
+corollary multiplicity_sum_min:
+ assumes "multiplicity p a \<noteq> multiplicity p b" "a \<noteq> 0" "b \<noteq> 0"
+ shows "multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)"
+proof -
+ let ?vp = "multiplicity p"
+ from assms have "?vp a < ?vp b \<or> ?vp a > ?vp b"
+ by auto
+ then show ?thesis
+ by (metis assms multiplicity_sum_lt min.commute add_commute min.strict_order_iff)
+qed
+
end
end
--- a/src/HOL/Equiv_Relations.thy Sat Jan 30 20:47:00 2021 +0100
+++ b/src/HOL/Equiv_Relations.thy Sat Jan 30 21:43:13 2021 +0100
@@ -355,6 +355,50 @@
by (simp add: quotient_def card_UN_disjoint)
qed
+text \<open>By Jakub Kądziołka:\<close>
+
+lemma sum_fun_comp:
+ assumes "finite S" "finite R" "g ` S \<subseteq> R"
+ shows "(\<Sum>x \<in> S. f (g x)) = (\<Sum>y \<in> R. of_nat (card {x \<in> S. g x = y}) * f y)"
+proof -
+ let ?r = "relation_of (\<lambda>p q. g p = g q) S"
+ have eqv: "equiv S ?r"
+ unfolding relation_of_def by (auto intro: comp_equivI)
+ have finite: "C \<in> S//?r \<Longrightarrow> finite C" for C
+ by (fact finite_equiv_class[OF `finite S` equiv_type[OF `equiv S ?r`]])
+ have disjoint: "A \<in> S//?r \<Longrightarrow> B \<in> S//?r \<Longrightarrow> A \<noteq> B \<Longrightarrow> A \<inter> B = {}" for A B
+ using eqv quotient_disj by blast
+
+ let ?cls = "\<lambda>y. {x \<in> S. y = g x}"
+ have quot_as_img: "S//?r = ?cls ` g ` S"
+ by (auto simp add: relation_of_def quotient_def)
+ have cls_inj: "inj_on ?cls (g ` S)"
+ by (auto intro: inj_onI)
+
+ have rest_0: "(\<Sum>y \<in> R - g ` S. of_nat (card (?cls y)) * f y) = 0"
+ proof -
+ have "of_nat (card (?cls y)) * f y = 0" if asm: "y \<in> R - g ` S" for y
+ proof -
+ from asm have *: "?cls y = {}" by auto
+ show ?thesis unfolding * by simp
+ qed
+ thus ?thesis by simp
+ qed
+
+ have "(\<Sum>x \<in> S. f (g x)) = (\<Sum>C \<in> S//?r. \<Sum>x \<in> C. f (g x))"
+ using eqv finite disjoint
+ by (simp flip: sum.Union_disjoint[simplified] add: Union_quotient)
+ also have "... = (\<Sum>y \<in> g ` S. \<Sum>x \<in> ?cls y. f (g x))"
+ unfolding quot_as_img by (simp add: sum.reindex[OF cls_inj])
+ also have "... = (\<Sum>y \<in> g ` S. \<Sum>x \<in> ?cls y. f y)"
+ by auto
+ also have "... = (\<Sum>y \<in> g ` S. of_nat (card (?cls y)) * f y)"
+ by (simp flip: sum_constant)
+ also have "... = (\<Sum>y \<in> R. of_nat (card (?cls y)) * f y)"
+ using rest_0 by (simp add: sum.subset_diff[OF \<open>g ` S \<subseteq> R\<close> \<open>finite R\<close>])
+ finally show ?thesis
+ by (simp add: eq_commute)
+qed
subsection \<open>Projection\<close>
--- a/src/HOL/Library/Sublist.thy Sat Jan 30 20:47:00 2021 +0100
+++ b/src/HOL/Library/Sublist.thy Sat Jan 30 21:43:13 2021 +0100
@@ -476,40 +476,19 @@
obtains "prefix xs ys" | "strict_prefix ys xs" | "xs \<parallel> ys"
unfolding parallel_def strict_prefix_def by blast
+lemma parallel_cancel: "a#xs \<parallel> a#ys \<Longrightarrow> xs \<parallel> ys"
+ by (simp add: parallel_def)
+
theorem parallel_decomp:
"xs \<parallel> ys \<Longrightarrow> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs"
-proof (induct xs rule: rev_induct)
- case Nil
- then have False by auto
- then show ?case ..
-next
- case (snoc x xs)
- show ?case
- proof (rule prefix_cases)
- assume le: "prefix xs ys"
- then obtain ys' where ys: "ys = xs @ ys'" ..
- show ?thesis
- proof (cases ys')
- assume "ys' = []"
- then show ?thesis by (metis append_Nil2 parallelE prefixI snoc.prems ys)
- next
- fix c cs assume ys': "ys' = c # cs"
- have "x \<noteq> c" using snoc.prems ys ys' by fastforce
- thus "\<exists>as b bs c cs. b \<noteq> c \<and> xs @ [x] = as @ b # bs \<and> ys = as @ c # cs"
- using ys ys' by blast
- qed
- next
- assume "strict_prefix ys xs"
- then have "prefix ys (xs @ [x])" by (simp add: strict_prefix_def)
- with snoc have False by blast
- then show ?thesis ..
- next
- assume "xs \<parallel> ys"
- with snoc obtain as b bs c cs where neq: "(b::'a) \<noteq> c"
- and xs: "xs = as @ b # bs" and ys: "ys = as @ c # cs"
- by blast
- from xs have "xs @ [x] = as @ b # (bs @ [x])" by simp
- with neq ys show ?thesis by blast
+proof (induct rule: list_induct2', blast, force, force)
+ case (4 x xs y ys)
+ then show ?case
+ proof (cases "x \<noteq> y", blast)
+ assume "\<not> x \<noteq> y" hence "x = y" by blast
+ then show ?thesis
+ using "4.hyps"[OF parallel_cancel[OF "4.prems"[folded \<open>x = y\<close>]]]
+ by (meson Cons_eq_appendI)
qed
qed
--- a/src/HOL/Set_Interval.thy Sat Jan 30 20:47:00 2021 +0100
+++ b/src/HOL/Set_Interval.thy Sat Jan 30 21:43:13 2021 +0100
@@ -1545,6 +1545,18 @@
finally show ?thesis.
qed
+lemma card_le_Suc_Max: "finite S \<Longrightarrow> card S \<le> Suc (Max S)"
+proof (rule classical)
+ assume "finite S" and "\<not> Suc (Max S) \<ge> card S"
+ then have "Suc (Max S) < card S"
+ by simp
+ with `finite S` have "S \<subseteq> {0..Max S}"
+ by auto
+ hence "card S \<le> card {0..Max S}"
+ by (intro card_mono; auto)
+ thus "card S \<le> Suc (Max S)"
+ by simp
+qed
subsection \<open>Lemmas useful with the summation operator sum\<close>
@@ -2057,6 +2069,30 @@
end
+lemma card_sum_le_nat_sum: "\<Sum> {0..<card S} \<le> \<Sum> S"
+proof (cases "finite S")
+ case True
+ then show ?thesis
+ proof (induction "card S" arbitrary: S)
+ case (Suc x)
+ then have "Max S \<ge> x" using card_le_Suc_Max by fastforce
+ let ?S' = "S - {Max S}"
+ from Suc have "Max S \<in> S" by (auto intro: Max_in)
+ hence cards: "card S = Suc (card ?S')"
+ using `finite S` by (intro card.remove; auto)
+ hence "\<Sum> {0..<card ?S'} \<le> \<Sum> ?S'"
+ using Suc by (intro Suc; auto)
+
+ hence "\<Sum> {0..<card ?S'} + x \<le> \<Sum> ?S' + Max S"
+ using `Max S \<ge> x` by simp
+ also have "... = \<Sum> S"
+ using sum.remove[OF `finite S` `Max S \<in> S`, where g="\<lambda>x. x"]
+ by simp
+ finally show ?case
+ using cards Suc by auto
+ qed simp
+qed simp
+
lemma sum_natinterval_diff:
fixes f:: "nat \<Rightarrow> ('a::ab_group_add)"
shows "sum (\<lambda>k. f k - f(k + 1)) {(m::nat) .. n} =
--- a/src/Pure/Admin/build_history.scala Sat Jan 30 20:47:00 2021 +0100
+++ b/src/Pure/Admin/build_history.scala Sat Jan 30 21:43:13 2021 +0100
@@ -161,8 +161,12 @@
val (afp_build_args, afp_sessions) =
if (afp_rev.isEmpty) (Nil, Nil)
else {
- val afp = AFP.init(options, afp_repos)
- (List("-d", "~~/AFP/thys"), afp.partition(afp_partition))
+ val (opt, sessions) =
+ try {
+ val afp = AFP.init(options, afp_repos)
+ ("-d", afp.partition(afp_partition))
+ } catch { case ERROR(_) => ("-D", Nil) }
+ (List(opt, "~~/AFP/thys"), sessions)
}
@@ -570,7 +574,7 @@
else {
val afp_repos = isabelle_repos_other + Path.explode("AFP")
Mercurial.setup_repository(afp_repos_source, afp_repos, ssh = ssh)
- " -A " + Bash.string(afp_rev.get)
+ " -A " + Bash.string(afp_rev.get)
}
@@ -580,11 +584,19 @@
{
val output_file = tmp_dir + Path.explode("output")
- execute("Admin/build_history",
- "-o " + ssh.bash_path(output_file) +
- (if (rev == "") "" else " -r " + Bash.string(rev_id)) + " " +
- options + afp_options + " " + ssh.bash_path(isabelle_repos_other) + " " + args,
- echo = true, strict = false)
+ val rev_options = if (rev == "") "" else " -r " + Bash.string(rev_id)
+
+ try {
+ execute("Admin/build_history",
+ "-o " + ssh.bash_path(output_file) + rev_options + afp_options + " " + options + " " +
+ ssh.bash_path(isabelle_repos_other) + " " + args,
+ echo = true, strict = false)
+ }
+ catch {
+ case ERROR(msg) =>
+ cat_error(msg,
+ "The error(s) above occurred for build_bistory " + rev_options + afp_options)
+ }
for (line <- split_lines(ssh.read(output_file)))
yield {
--- a/src/Pure/Admin/isabelle_cronjob.scala Sat Jan 30 20:47:00 2021 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala Sat Jan 30 21:43:13 2021 +0100
@@ -104,7 +104,7 @@
isabelle_identifier = "cronjob_build_history",
self_update = true,
rev = "build_history_base",
- options = "-f",
+ options = "-C '$USER_HOME/.isabelle/contrib' -f",
args = "HOL")
for ((log_name, bytes) <- results) {
@@ -326,6 +326,14 @@
options = "-m32 -B -M1,2,4 -e ISABELLE_GHC_SETUP=true -p pide_session=false",
self_update = true, args = "-a -d '~~/src/Benchmarks'")),
List(
+ Remote_Build("macOS 11.1 Big Sur", "mini1",
+ options = "-m32 -B -M1x2,2,4 -p pide_session=false" +
+ " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
+ " -e ISABELLE_GHC_SETUP=true" +
+ " -e ISABELLE_MLTON=/usr/local/bin/mlton" +
+ " -e ISABELLE_SMLNJ=/usr/local/smlnj/bin/sml" +
+ " -e ISABELLE_SWIPL=/usr/local/bin/swipl",
+ self_update = true, args = "-a -d '~~/src/Benchmarks'"),
Remote_Build("macOS 10.14 Mojave", "mini2",
options = "-m32 -B -M1x2,2,4 -p pide_session=false" +
" -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
@@ -407,6 +415,7 @@
rev = rev,
afp_rev = afp_rev,
options =
+ " -C '$USER_HOME/.isabelle/contrib'" +
" -N " + Bash.string(task_name) + (if (i < 0) "" else "_" + (i + 1).toString) +
" -f -h " + Bash.string(r.host) + " " +
(r.java_heap match {