# HG changeset patch
# User wenzelm
# Date 1612039393 -3600
# Node ID 8c98e497492a043624572f414e8e2ad1c9b84193
# Parent  de16d797adbef88635e62a85ed4048328eb6c0a6# Parent  ce90865dbaeb4ce4c3d4d974b2a0ebf8ee135979
merged

diff -r de16d797adbe -r 8c98e497492a Admin/PLATFORMS
--- 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)
diff -r de16d797adbe -r 8c98e497492a CONTRIBUTORS
--- 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
 -----------------------------
 
diff -r de16d797adbe -r 8c98e497492a src/HOL/Computational_Algebra/Factorial_Ring.thy
--- 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
diff -r de16d797adbe -r 8c98e497492a src/HOL/Equiv_Relations.thy
--- 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>
 
diff -r de16d797adbe -r 8c98e497492a src/HOL/Library/Sublist.thy
--- 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
 
diff -r de16d797adbe -r 8c98e497492a src/HOL/Set_Interval.thy
--- 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} =
diff -r de16d797adbe -r 8c98e497492a src/Pure/Admin/build_history.scala
--- 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 {
diff -r de16d797adbe -r 8c98e497492a src/Pure/Admin/isabelle_cronjob.scala
--- 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 {