# HG changeset patch
# User wenzelm
# Date 1611513277 -3600
# Node ID ebf7babc05ce2649babc787d65dcdca0cab3f1de
# Parent  0398f18ec76c1729233a5adb6574f8968fc8edde# Parent  a8a8bc42d552208de2c11d7735a89c1e4958ed96
merged, with minor edits: Admin/PLATFORMS, CONTRIBUTORS;

diff -r a8a8bc42d552 -r ebf7babc05ce Admin/PLATFORMS
--- a/Admin/PLATFORMS	Sun Jan 24 17:39:29 2021 +0100
+++ b/Admin/PLATFORMS	Sun Jan 24 19:34:37 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)
diff -r a8a8bc42d552 -r ebf7babc05ce CONTRIBUTORS
--- a/CONTRIBUTORS	Sun Jan 24 17:39:29 2021 +0100
+++ b/CONTRIBUTORS	Sun Jan 24 19:34:37 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
 -----------------------------
 
diff -r a8a8bc42d552 -r ebf7babc05ce src/HOL/Computational_Algebra/Factorial_Ring.thy
--- a/src/HOL/Computational_Algebra/Factorial_Ring.thy	Sun Jan 24 17:39:29 2021 +0100
+++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy	Sun Jan 24 19:34:37 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
diff -r a8a8bc42d552 -r ebf7babc05ce src/HOL/Equiv_Relations.thy
--- a/src/HOL/Equiv_Relations.thy	Sun Jan 24 17:39:29 2021 +0100
+++ b/src/HOL/Equiv_Relations.thy	Sun Jan 24 19:34:37 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>
 
diff -r a8a8bc42d552 -r ebf7babc05ce src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Sun Jan 24 17:39:29 2021 +0100
+++ b/src/HOL/Set_Interval.thy	Sun Jan 24 19:34:37 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} =
diff -r a8a8bc42d552 -r ebf7babc05ce src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Sun Jan 24 17:39:29 2021 +0100
+++ b/src/Pure/Admin/build_history.scala	Sun Jan 24 19:34:37 2021 +0100
@@ -570,7 +570,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 +580,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 {
diff -r a8a8bc42d552 -r ebf7babc05ce src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Sun Jan 24 17:39:29 2021 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Sun Jan 24 19:34:37 2021 +0100
@@ -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" +