merged;

--- a/NEWS	Sat Aug 20 21:33:51 2022 +0200
+++ b/NEWS	Sat Aug 20 21:34:55 2022 +0200
@@ -34,12 +34,15 @@
 
 *** HOL ***
 
+* Renamed attribute "arith_split" to "linarith_split".  Minor
+INCOMPATIBILITY.
+
 * Theory Char_ord: streamlined logical specifications.
 Minor INCOMPATIBILITY.
 
 * New Theory Code_Abstract_Char implements characters by target language
 integers, sacrificing pattern patching in exchange for dramatically
-increased performance for comparisions.
+increased performance for comparisons.
 
 * New theory HOL-Library.NList of fixed length lists
 
@@ -49,6 +52,9 @@
 * Theory "HOL.Bit_Operations": rule bit_0 is not default [simp] any
 longer. INCOMPATIBILITY.
 
+* Streamlined primitive definitions of division and modulus on integers.
+INCOMPATIBILITY.
+
 * Theory "HOL.Fun":
   - Added predicate monotone_on and redefined monotone to be an
     abbreviation. Lemma monotone_def is explicitly provided for backward
@@ -146,6 +152,8 @@
   - Added support for TX0 and TX1 TPTP formats and $ite/$let expressions
     in TH0 and TH1.
   - Added support for cvc5.
+  - Generate Isar proofs by default when and only when the one-liner proof
+    fails to replay and the Isar proof succeeds.
   - Replaced option "sledgehammer_atp_dest_dir" by
     "sledgehammer_atp_problem_dest_dir", for problem files, and
     "sledgehammer_atp_proof_dest_dir", for proof files. Minor INCOMPATIBILITY.

--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Sat Aug 20 21:33:51 2022 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Sat Aug 20 21:34:55 2022 +0200
@@ -2003,7 +2003,7 @@
   \begin{matharray}{rcl}
     @{method_def (HOL) arith} & : & \<open>method\<close> \\
     @{attribute_def (HOL) arith} & : & \<open>attribute\<close> \\
-    @{attribute_def (HOL) arith_split} & : & \<open>attribute\<close> \\
+    @{attribute_def (HOL) linarith_split} & : & \<open>attribute\<close> \\
   \end{matharray}
 
   \<^descr> @{method (HOL) arith} decides linear arithmetic problems (on types \<open>nat\<close>,
@@ -2013,7 +2013,7 @@
   \<^descr> @{attribute (HOL) arith} declares facts that are supplied to the
   arithmetic provers implicitly.
 
-  \<^descr> @{attribute (HOL) arith_split} attribute declares case split rules to be
+  \<^descr> @{attribute (HOL) linarith_split} attribute declares case split rules to be
   expanded before @{method (HOL) arith} is invoked.
 
 

--- a/src/Doc/Sledgehammer/document/root.tex	Sat Aug 20 21:33:51 2022 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Sat Aug 20 21:34:55 2022 +0200
@@ -1129,9 +1129,9 @@
 \opsmart{isar\_proofs}{no\_isar\_proofs}
 Specifies whether Isar proofs should be output in addition to one-line proofs.
 The construction of Isar proof is still experimental and may sometimes fail;
-however, when they succeed they are usually faster and more intelligible than
-one-line proofs. If the option is set to \textit{smart} (the default), Isar
-proofs are only generated when no working one-line proof is available.
+however, when they succeed they can be faster and sometimes more intelligible
+than one-line proofs. If the option is set to \textit{smart} (the default), Isar
+proofs are generated only when no working one-line proof is available.
 
 \opdefault{compress}{int}{smart}
 Specifies the granularity of the generated Isar proofs if \textit{isar\_proofs}
@@ -1191,14 +1191,13 @@
 Specifies the maximum number of seconds that the automatic provers should spend
 searching for a proof. This excludes problem preparation and is a soft limit.
 
-\opdefault{slices}{int}{\upshape 6 times the number of cores detected}
-Specifies the number of time slices. Each time slice corresponds to a prover
-invocation and has its own set of options. For example, for SPASS, one slice
-might specify the fast but incomplete set-of-support (SOS) strategy with 100
-relevant lemmas, whereas other slices might run without SOS and with 500 lemmas.
-Slicing (and thereby parallelism) can be disable by setting \textit{slices} to
-1. Since slicing is a valuable optimization, you should probably leave it
-enabled unless you are conducting experiments.
+\opdefault{slices}{int}{\upshape 12 times the number of cores detected}
+Specifies the number of time slices. Time slices are the basic unit for prover
+invocations. They are divided among the available provers. A single prover
+invocation can occupy a single slice, two slices, or more, depending on the
+prover. Slicing (and thereby parallelism) can be disable by setting
+\textit{slices} to 1. Since slicing is a valuable optimization, you should
+probably leave it enabled unless you are conducting experiments.
 
 \nopagebreak
 {\small See also \textit{verbose} (\S\ref{output-format}).}

--- a/src/HOL/Archimedean_Field.thy	Sat Aug 20 21:33:51 2022 +0200
+++ b/src/HOL/Archimedean_Field.thy	Sat Aug 20 21:34:55 2022 +0200
@@ -243,7 +243,7 @@
 lemma floor_le_iff: "\<lfloor>x\<rfloor> \<le> z \<longleftrightarrow> x < of_int z + 1"
   by (simp add: not_less [symmetric] less_floor_iff)
 
-lemma floor_split[arith_split]: "P \<lfloor>t\<rfloor> \<longleftrightarrow> (\<forall>i. of_int i \<le> t \<and> t < of_int i + 1 \<longrightarrow> P i)"
+lemma floor_split[linarith_split]: "P \<lfloor>t\<rfloor> \<longleftrightarrow> (\<forall>i. of_int i \<le> t \<and> t < of_int i + 1 \<longrightarrow> P i)"
   by (metis floor_correct floor_unique less_floor_iff not_le order_refl)
 
 lemma floor_mono:
@@ -618,7 +618,7 @@
 lemma ceiling_diff_one [simp]: "\<lceil>x - 1\<rceil> = \<lceil>x\<rceil> - 1"
   using ceiling_diff_of_int [of x 1] by simp
 
-lemma ceiling_split[arith_split]: "P \<lceil>t\<rceil> \<longleftrightarrow> (\<forall>i. of_int i - 1 < t \<and> t \<le> of_int i \<longrightarrow> P i)"
+lemma ceiling_split[linarith_split]: "P \<lceil>t\<rceil> \<longleftrightarrow> (\<forall>i. of_int i - 1 < t \<and> t \<le> of_int i \<longrightarrow> P i)"
   by (auto simp add: ceiling_unique ceiling_correct)
 
 lemma ceiling_diff_floor_le_1: "\<lceil>x\<rceil> - \<lfloor>x\<rfloor> \<le> 1"

--- a/src/HOL/Bit_Operations.thy	Sat Aug 20 21:33:51 2022 +0200
+++ b/src/HOL/Bit_Operations.thy	Sat Aug 20 21:34:55 2022 +0200
@@ -1465,7 +1465,7 @@
 
 lemma not_int_div_2:
   \<open>NOT k div 2 = NOT (k div 2)\<close> for k :: int
-  by (cases k) (simp_all add: not_int_def divide_int_def nat_add_distrib)
+  by (simp add: not_int_def)
 
 lemma bit_not_int_iff:
   \<open>bit (NOT k) n \<longleftrightarrow> \<not> bit k n\<close>
@@ -1729,7 +1729,7 @@
   case (odd k)
   from odd.IH [of \<open>l div 2\<close>] odd.hyps odd.prems
   show ?case
-    by (simp add: and_int_rec [of _ l]) linarith
+    by (simp add: and_int_rec [of _ l])
 qed
 
 lemma or_nonnegative_int_iff [simp]:
@@ -1754,7 +1754,7 @@
   case (even k)
   from even.IH [of \<open>l div 2\<close>] even.hyps even.prems
   show ?case
-    by (simp add: or_int_rec [of _ l]) linarith
+    by (simp add: or_int_rec [of _ l])
 next
   case (odd k)
   from odd.IH [of \<open>l div 2\<close>] odd.hyps odd.prems
@@ -2173,22 +2173,6 @@
   \<open>\<not> 2 ^ n \<le> (0::int)\<close>
   by (simp add: power_le_zero_eq)
 
-lemma half_nonnegative_int_iff [simp]:
-  \<open>k div 2 \<ge> 0 \<longleftrightarrow> k \<ge> 0\<close> for k :: int
-proof (cases \<open>k \<ge> 0\<close>)
-  case True
-  then show ?thesis
-    by (auto simp add: divide_int_def sgn_1_pos)
-next
-  case False
-  then show ?thesis
-    by (auto simp add: divide_int_def not_le elim!: evenE)
-qed
-
-lemma half_negative_int_iff [simp]:
-  \<open>k div 2 < 0 \<longleftrightarrow> k < 0\<close> for k :: int
-  by (subst Not_eq_iff [symmetric]) (simp add: not_less)
-
 lemma int_bit_bound:
   fixes k :: int
   obtains n where \<open>\<And>m. n \<le> m \<Longrightarrow> bit k m \<longleftrightarrow> bit k n\<close>

--- a/src/HOL/Code_Numeral.thy	Sat Aug 20 21:33:51 2022 +0200
+++ b/src/HOL/Code_Numeral.thy	Sat Aug 20 21:34:55 2022 +0200
@@ -385,17 +385,17 @@
 where
   divmod_integer'_def: "divmod_integer m n = (numeral m div numeral n, numeral m mod numeral n)"
 
-definition divmod_step_integer :: "num \<Rightarrow> integer \<times> integer \<Rightarrow> integer \<times> integer"
+definition divmod_step_integer :: "integer \<Rightarrow> integer \<times> integer \<Rightarrow> integer \<times> integer"
 where
   "divmod_step_integer l qr = (let (q, r) = qr
-    in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
+    in if r \<ge> l then (2 * q + 1, r - l)
     else (2 * q, r))"
 
 instance proof
   show "divmod m n = (numeral m div numeral n :: integer, numeral m mod numeral n)"
     for m n by (fact divmod_integer'_def)
   show "divmod_step l qr = (let (q, r) = qr
-    in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
+    in if r \<ge> l then (2 * q + 1, r - l)
     else (2 * q, r))" for l and qr :: "integer \<times> integer"
     by (fact divmod_step_integer_def)
 qed (transfer,

--- a/src/HOL/Divides.thy	Sat Aug 20 21:33:51 2022 +0200
+++ b/src/HOL/Divides.thy	Sat Aug 20 21:34:55 2022 +0200
@@ -11,19 +11,7 @@
 
 subsection \<open>More on division\<close>
 
-inductive eucl_rel_int :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool"
-  where eucl_rel_int_by0: "eucl_rel_int k 0 (0, k)"
-  | eucl_rel_int_dividesI: "l \<noteq> 0 \<Longrightarrow> k = q * l \<Longrightarrow> eucl_rel_int k l (q, 0)"
-  | eucl_rel_int_remainderI: "sgn r = sgn l \<Longrightarrow> \<bar>r\<bar> < \<bar>l\<bar>
-      \<Longrightarrow> k = q * l + r \<Longrightarrow> eucl_rel_int k l (q, r)"
-
-lemma eucl_rel_int_iff:    
-  "eucl_rel_int k l (q, r) \<longleftrightarrow> 
-    k = l * q + r \<and>
-     (if 0 < l then 0 \<le> r \<and> r < l else if l < 0 then l < r \<and> r \<le> 0 else q = 0)"
-  by (cases "r = 0")
-    (auto elim!: eucl_rel_int.cases intro: eucl_rel_int_by0 eucl_rel_int_dividesI eucl_rel_int_remainderI
-    simp add: ac_simps sgn_1_pos sgn_1_neg)
+subsubsection \<open>Monotonicity in the First Argument (Dividend)\<close>
 
 lemma unique_quotient_lemma:
   assumes "b * q' + r' \<le> b * q + r" "0 \<le> r'" "r' < b" "r < b" shows "q' \<le> (q::int)"
@@ -42,188 +30,14 @@
   "b * q' + r' \<le> b*q + r \<Longrightarrow> r \<le> 0 \<Longrightarrow> b < r \<Longrightarrow> b < r' \<Longrightarrow> q \<le> (q'::int)"
   using unique_quotient_lemma[where b = "-b" and r = "-r'" and r'="-r"] by auto
 
-lemma unique_quotient:
-  "eucl_rel_int a b (q, r) \<Longrightarrow> eucl_rel_int a b (q', r') \<Longrightarrow> q = q'"
-  apply (rule order_antisym)
-   apply (simp_all add: eucl_rel_int_iff linorder_neq_iff split: if_split_asm)
-     apply (blast intro: order_eq_refl [THEN unique_quotient_lemma] order_eq_refl [THEN unique_quotient_lemma_neg] sym)+
-  done
-
-lemma unique_remainder:
-  assumes "eucl_rel_int a b (q, r)"
-    and "eucl_rel_int a b (q', r')"
-  shows "r = r'"
-proof -
-  have "q = q'"
-    using assms by (blast intro: unique_quotient)
-  then show "r = r'"
-    using assms by (simp add: eucl_rel_int_iff)
-qed
-
-lemma eucl_rel_int:
-  "eucl_rel_int k l (k div l, k mod l)"
-proof (cases k rule: int_cases3)
-  case zero
-  then show ?thesis
-    by (simp add: eucl_rel_int_iff divide_int_def modulo_int_def)
-next
-  case (pos n)
-  then show ?thesis
-    using div_mult_mod_eq [of n]
-    by (cases l rule: int_cases3)
-      (auto simp del: of_nat_mult of_nat_add
-        simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
-        eucl_rel_int_iff divide_int_def modulo_int_def)
-next
-  case (neg n)
-  then show ?thesis
-    using div_mult_mod_eq [of n]
-    by (cases l rule: int_cases3)
-      (auto simp del: of_nat_mult of_nat_add
-        simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
-        eucl_rel_int_iff divide_int_def modulo_int_def)
-qed
-
-lemma divmod_int_unique:
-  assumes "eucl_rel_int k l (q, r)"
-  shows div_int_unique: "k div l = q" and mod_int_unique: "k mod l = r"
-  using assms eucl_rel_int [of k l]
-  using unique_quotient [of k l] unique_remainder [of k l]
-  by auto
-
-lemma div_abs_eq_div_nat:
-  "\<bar>k\<bar> div \<bar>l\<bar> = int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)"
-  by (simp add: divide_int_def)
-
-lemma mod_abs_eq_div_nat:
-  "\<bar>k\<bar> mod \<bar>l\<bar> = int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)"
-  by (simp add: modulo_int_def)
-
-lemma zdiv_int:
-  "int (a div b) = int a div int b"
-  by (simp add: divide_int_def)
-
-lemma zmod_int:
-  "int (a mod b) = int a mod int b"
-  by (simp add: modulo_int_def)
-
-lemma div_sgn_abs_cancel:
-  fixes k l v :: int
-  assumes "v \<noteq> 0"
-  shows "(sgn v * \<bar>k\<bar>) div (sgn v * \<bar>l\<bar>) = \<bar>k\<bar> div \<bar>l\<bar>"
-proof -
-  from assms have "sgn v = - 1 \<or> sgn v = 1"
-    by (cases "v \<ge> 0") auto
-  then show ?thesis
-    using assms unfolding divide_int_def [of "sgn v * \<bar>k\<bar>" "sgn v * \<bar>l\<bar>"]
-    by (fastforce simp add: not_less div_abs_eq_div_nat)
-qed
-
-lemma div_eq_sgn_abs:
-  fixes k l v :: int
-  assumes "sgn k = sgn l"
-  shows "k div l = \<bar>k\<bar> div \<bar>l\<bar>"
-proof (cases "l = 0")
-  case True
-  then show ?thesis
-    by simp
-next
-  case False
-  with assms have "(sgn k * \<bar>k\<bar>) div (sgn l * \<bar>l\<bar>) = \<bar>k\<bar> div \<bar>l\<bar>"
-    using div_sgn_abs_cancel [of l k l] by simp
-  then show ?thesis
-    by (simp add: sgn_mult_abs)
-qed
-
-lemma div_dvd_sgn_abs:
-  fixes k l :: int
-  assumes "l dvd k"
-  shows "k div l = (sgn k * sgn l) * (\<bar>k\<bar> div \<bar>l\<bar>)"
-proof (cases "k = 0 \<or> l = 0")
-  case True
-  then show ?thesis
-    by auto
-next
-  case False
-  then have "k \<noteq> 0" and "l \<noteq> 0"
-    by auto
-  show ?thesis
-  proof (cases "sgn l = sgn k")
-    case True
-    then show ?thesis
-      by (auto simp add: div_eq_sgn_abs)
-  next
-    case False
-    with \<open>k \<noteq> 0\<close> \<open>l \<noteq> 0\<close>
-    have "sgn l * sgn k = - 1"
-      by (simp add: sgn_if split: if_splits)
-    with assms show ?thesis
-      unfolding divide_int_def [of k l]
-      by (auto simp add: zdiv_int ac_simps)
-  qed
-qed
-
-lemma div_noneq_sgn_abs:
-  fixes k l :: int
-  assumes "l \<noteq> 0"
-  assumes "sgn k \<noteq> sgn l"
-  shows "k div l = - (\<bar>k\<bar> div \<bar>l\<bar>) - of_bool (\<not> l dvd k)"
-  using assms
-  by (simp only: divide_int_def [of k l], auto simp add: not_less zdiv_int)
-  
-
-subsubsection \<open>Laws for div and mod with Unary Minus\<close>
-
-lemma zminus1_lemma:
-     "eucl_rel_int a b (q, r) ==> b \<noteq> 0
-      ==> eucl_rel_int (-a) b (if r=0 then -q else -q - 1,
-                          if r=0 then 0 else b-r)"
-by (force simp add: eucl_rel_int_iff right_diff_distrib)
-
-
-lemma zdiv_zminus1_eq_if:
-     "b \<noteq> (0::int)
-      \<Longrightarrow> (-a) div b = (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
-by (blast intro: eucl_rel_int [THEN zminus1_lemma, THEN div_int_unique])
-
-lemma zmod_zminus1_eq_if:
-     "(-a::int) mod b = (if a mod b = 0 then 0 else  b - (a mod b))"
-proof (cases "b = 0")
-  case False
-  then show ?thesis
-    by (blast intro: eucl_rel_int [THEN zminus1_lemma, THEN mod_int_unique])
-qed auto
-
-lemma zmod_zminus1_not_zero:
-  fixes k l :: int
-  shows "- k mod l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
-  by (simp add: mod_eq_0_iff_dvd)
-
-lemma zmod_zminus2_not_zero:
-  fixes k l :: int
-  shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
-  by (simp add: mod_eq_0_iff_dvd)
-
-lemma zdiv_zminus2_eq_if:
-  "b \<noteq> (0::int)
-      ==> a div (-b) =
-          (if a mod b = 0 then - (a div b) else  - (a div b) - 1)"
-  by (auto simp add: zdiv_zminus1_eq_if div_minus_right)
-
-lemma zmod_zminus2_eq_if:
-  "a mod (-b::int) = (if a mod b = 0 then 0 else  (a mod b) - b)"
-  by (auto simp add: zmod_zminus1_eq_if mod_minus_right)
-
-
-subsubsection \<open>Monotonicity in the First Argument (Dividend)\<close>
-
 lemma zdiv_mono1:
-  fixes b::int
-  assumes "a \<le> a'" "0 < b" shows "a div b \<le> a' div b"
+  \<open>a div b \<le> a' div b\<close>
+  if \<open>a \<le> a'\<close> \<open>0 < b\<close>
+  for a b b' :: int
 proof (rule unique_quotient_lemma)
   show "b * (a div b) + a mod b \<le> b * (a' div b) + a' mod b"
-    using assms(1) by auto
-qed (use assms in auto)
+    using \<open>a \<le> a'\<close> by auto
+qed (use that in auto)
 
 lemma zdiv_mono1_neg:
   fixes b::int
@@ -299,6 +113,72 @@
     by simp
 qed (use assms in auto)
 
+
+subsubsection \<open>Computing \<open>div\<close> and \<open>mod\<close> with shifting\<close>
+
+inductive eucl_rel_int :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool"
+  where eucl_rel_int_by0: "eucl_rel_int k 0 (0, k)"
+  | eucl_rel_int_dividesI: "l \<noteq> 0 \<Longrightarrow> k = q * l \<Longrightarrow> eucl_rel_int k l (q, 0)"
+  | eucl_rel_int_remainderI: "sgn r = sgn l \<Longrightarrow> \<bar>r\<bar> < \<bar>l\<bar>
+      \<Longrightarrow> k = q * l + r \<Longrightarrow> eucl_rel_int k l (q, r)"
+
+lemma eucl_rel_int_iff:    
+  "eucl_rel_int k l (q, r) \<longleftrightarrow> 
+    k = l * q + r \<and>
+     (if 0 < l then 0 \<le> r \<and> r < l else if l < 0 then l < r \<and> r \<le> 0 else q = 0)"
+  by (cases "r = 0")
+    (auto elim!: eucl_rel_int.cases intro: eucl_rel_int_by0 eucl_rel_int_dividesI eucl_rel_int_remainderI
+    simp add: ac_simps sgn_1_pos sgn_1_neg)
+
+lemma unique_quotient:
+  "eucl_rel_int a b (q, r) \<Longrightarrow> eucl_rel_int a b (q', r') \<Longrightarrow> q = q'"
+  apply (rule order_antisym)
+   apply (simp_all add: eucl_rel_int_iff linorder_neq_iff split: if_split_asm)
+     apply (blast intro: order_eq_refl [THEN unique_quotient_lemma] order_eq_refl [THEN unique_quotient_lemma_neg] sym)+
+  done
+
+lemma unique_remainder:
+  assumes "eucl_rel_int a b (q, r)"
+    and "eucl_rel_int a b (q', r')"
+  shows "r = r'"
+proof -
+  have "q = q'"
+    using assms by (blast intro: unique_quotient)
+  then show "r = r'"
+    using assms by (simp add: eucl_rel_int_iff)
+qed
+
+lemma eucl_rel_int:
+  "eucl_rel_int k l (k div l, k mod l)"
+proof (cases k rule: int_cases3)
+  case zero
+  then show ?thesis
+    by (simp add: eucl_rel_int_iff divide_int_def modulo_int_def)
+next
+  case (pos n)
+  then show ?thesis
+    using div_mult_mod_eq [of n]
+    by (cases l rule: int_cases3)
+      (auto simp del: of_nat_mult of_nat_add
+        simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
+        eucl_rel_int_iff divide_int_def modulo_int_def)
+next
+  case (neg n)
+  then show ?thesis
+    using div_mult_mod_eq [of n]
+    by (cases l rule: int_cases3)
+      (auto simp del: of_nat_mult of_nat_add
+        simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
+        eucl_rel_int_iff divide_int_def modulo_int_def)
+qed
+
+lemma divmod_int_unique:
+  assumes "eucl_rel_int k l (q, r)"
+  shows div_int_unique: "k div l = q" and mod_int_unique: "k mod l = r"
+  using assms eucl_rel_int [of k l]
+  using unique_quotient [of k l] unique_remainder [of k l]
+  by auto
+
 lemma div_pos_geq:
   fixes k l :: int
   assumes "0 < l" and "l \<le> k"
@@ -319,54 +199,6 @@
   with assms show ?thesis by simp
 qed
 
-
-subsubsection \<open>Splitting Rules for div and mod\<close>
-
-text\<open>The proofs of the two lemmas below are essentially identical\<close>
-
-lemma split_pos_lemma:
- "0<k \<Longrightarrow>
-    P(n div k :: int)(n mod k) = (\<forall>i j. 0\<le>j \<and> j<k \<and> n = k*i + j \<longrightarrow> P i j)"
-  by auto
-
-lemma split_neg_lemma:
- "k<0 \<Longrightarrow>
-    P(n div k :: int)(n mod k) = (\<forall>i j. k<j \<and> j\<le>0 \<and> n = k*i + j \<longrightarrow> P i j)"
-  by auto
-
-lemma split_zdiv:
- "P(n div k :: int) =
-  ((k = 0 \<longrightarrow> P 0) \<and>
-   (0<k \<longrightarrow> (\<forall>i j. 0\<le>j \<and> j<k \<and> n = k*i + j \<longrightarrow> P i)) \<and>
-   (k<0 \<longrightarrow> (\<forall>i j. k<j \<and> j\<le>0 \<and> n = k*i + j \<longrightarrow> P i)))"
-proof (cases "k = 0")
-  case False
-  then show ?thesis
-    unfolding linorder_neq_iff
-    by (auto simp add: split_pos_lemma [of concl: "\<lambda>x y. P x"] split_neg_lemma [of concl: "\<lambda>x y. P x"])
-qed auto
-
-lemma split_zmod:
- "P(n mod k :: int) =
-  ((k = 0 \<longrightarrow> P n) \<and>
-   (0<k \<longrightarrow> (\<forall>i j. 0\<le>j \<and> j<k \<and> n = k*i + j \<longrightarrow> P j)) \<and>
-   (k<0 \<longrightarrow> (\<forall>i j. k<j \<and> j\<le>0 \<and> n = k*i + j \<longrightarrow> P j)))"
-proof (cases "k = 0")
-  case False
-  then show ?thesis
-    unfolding linorder_neq_iff
-    by (auto simp add: split_pos_lemma [of concl: "\<lambda>x y. P y"] split_neg_lemma [of concl: "\<lambda>x y. P y"])
-qed auto
-
-text \<open>Enable (lin)arith to deal with \<^const>\<open>divide\<close> and \<^const>\<open>modulo\<close>
-  when these are applied to some constant that is of the form
-  \<^term>\<open>numeral k\<close>:\<close>
-declare split_zdiv [of _ _ "numeral k", arith_split] for k
-declare split_zmod [of _ _ "numeral k", arith_split] for k
-
-
-subsubsection \<open>Computing \<open>div\<close> and \<open>mod\<close> with shifting\<close>
-
 lemma pos_eucl_rel_int_mult_2:
   assumes "0 \<le> b"
   assumes "eucl_rel_int a b (q, r)"
@@ -430,31 +262,6 @@
   unfolding mult_2 [symmetric] add.commute [of _ 1]
   by (rule pos_zmod_mult_2, simp)
 
-lemma zdiv_eq_0_iff:
-  "i div k = 0 \<longleftrightarrow> k = 0 \<or> 0 \<le> i \<and> i < k \<or> i \<le> 0 \<and> k < i" (is "?L = ?R")
-  for i k :: int
-proof
-  assume ?L
-  moreover have "?L \<longrightarrow> ?R"
-    by (rule split_zdiv [THEN iffD2]) simp
-  ultimately show ?R
-    by blast
-next
-  assume ?R then show ?L
-    by auto
-qed
-
-lemma zmod_trivial_iff:
-  fixes i k :: int
-  shows "i mod k = i \<longleftrightarrow> k = 0 \<or> 0 \<le> i \<and> i < k \<or> i \<le> 0 \<and> k < i"
-proof -
-  have "i mod k = i \<longleftrightarrow> i div k = 0"
-    using div_mult_mod_eq [of i k] by safe auto
-  with zdiv_eq_0_iff
-  show ?thesis
-    by simp
-qed
-
   
 subsubsection \<open>Quotients of Signs\<close>
 
@@ -541,7 +348,6 @@
   "0<k \<Longrightarrow> 0 < (i::int) div k \<longleftrightarrow> k \<le> i"
   using pos_imp_zdiv_nonneg_iff[of k i] zdiv_eq_0_iff[of i k] by arith
 
-
 lemma neg_imp_zdiv_nonneg_iff:
   fixes a::int
   assumes "b < 0" 
@@ -574,6 +380,28 @@
 lemma zmod_le_nonneg_dividend: "(m::int) \<ge> 0 \<Longrightarrow> m mod k \<le> m"
   by (rule split_zmod[THEN iffD2]) (fastforce dest: q_pos_lemma intro: split_mult_pos_le)
 
+lemma sgn_div_eq_sgn_mult:
+  \<open>sgn (k div l) = of_bool (k div l \<noteq> 0) * sgn (k * l)\<close>
+  for k l :: int
+proof (cases \<open>k div l = 0\<close>)
+  case True
+  then show ?thesis
+    by simp
+next
+  case False
+  have \<open>0 \<le> \<bar>k\<bar> div \<bar>l\<bar>\<close>
+    by (cases \<open>l = 0\<close>) (simp_all add: pos_imp_zdiv_nonneg_iff)
+  then have \<open>\<bar>k\<bar> div \<bar>l\<bar> \<noteq> 0 \<longleftrightarrow> 0 < \<bar>k\<bar> div \<bar>l\<bar>\<close>
+    by (simp add: less_le)
+  also have \<open>\<dots> \<longleftrightarrow> \<bar>k\<bar> \<ge> \<bar>l\<bar>\<close>
+    using False nonneg1_imp_zdiv_pos_iff by auto
+  finally have *: \<open>\<bar>k\<bar> div \<bar>l\<bar> \<noteq> 0 \<longleftrightarrow> \<bar>l\<bar> \<le> \<bar>k\<bar>\<close> .
+  show ?thesis
+    using \<open>0 \<le> \<bar>k\<bar> div \<bar>l\<bar>\<close> False
+  by (auto simp add: div_eq_div_abs [of k l] div_eq_sgn_abs [of k l]
+    sgn_mult sgn_1_pos sgn_1_neg sgn_eq_0_iff nonneg1_imp_zdiv_pos_iff * dest: sgn_not_eq_imp)
+qed
+
 
 subsubsection \<open>Further properties\<close>
 
@@ -734,10 +562,10 @@
     and div_mult2_eq: "0 \<le> c \<Longrightarrow> a div (b * c) = a div b div c"
   assumes discrete: "a < b \<longleftrightarrow> a + 1 \<le> b"
   fixes divmod :: "num \<Rightarrow> num \<Rightarrow> 'a \<times> 'a"
-    and divmod_step :: "num \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<times> 'a"
+    and divmod_step :: "'a \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<times> 'a"
   assumes divmod_def: "divmod m n = (numeral m div numeral n, numeral m mod numeral n)"
     and divmod_step_def: "divmod_step l qr = (let (q, r) = qr
-    in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
+    in if r \<ge> l then (2 * q + 1, r - l)
     else (2 * q, r))"
     \<comment> \<open>These are conceptually definitions but force generated code
     to be monomorphic wrt. particular instances of this class which
@@ -824,8 +652,8 @@
 \<close>
 
 lemma divmod_step_eq [simp]:
-  "divmod_step l (q, r) = (if numeral l \<le> r
-    then (2 * q + 1, r - numeral l) else (2 * q, r))"
+  "divmod_step l (q, r) = (if l \<le> r
+    then (2 * q + 1, r - l) else (2 * q, r))"
   by (simp add: divmod_step_def)
 
 text \<open>
@@ -838,7 +666,7 @@
 
 lemma divmod_divmod_step:
   "divmod m n = (if m < n then (0, numeral m)
-    else divmod_step n (divmod m (Num.Bit0 n)))"
+    else divmod_step (numeral n) (divmod m (Num.Bit0 n)))"
 proof (cases "m < n")
   case True then have "numeral m < numeral n" by simp
   then show ?thesis
@@ -846,12 +674,12 @@
 next
   case False
   have "divmod m n =
-    divmod_step n (numeral m div (2 * numeral n),
+    divmod_step (numeral n) (numeral m div (2 * numeral n),
       numeral m mod (2 * numeral n))"
   proof (cases "numeral n \<le> numeral m mod (2 * numeral n)")
     case True
     with divmod_step_eq
-      have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) =
+      have "divmod_step (numeral n) (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) =
         (2 * (numeral m div (2 * numeral n)) + 1, numeral m mod (2 * numeral n) - numeral n)"
         by simp
     moreover from True divmod_digit_1 [of "numeral m" "numeral n"]
@@ -863,7 +691,7 @@
     case False then have *: "numeral m mod (2 * numeral n) < numeral n"
       by (simp add: not_le)
     with divmod_step_eq
-      have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) =
+      have "divmod_step (numeral n) (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) =
         (2 * (numeral m div (2 * numeral n)), numeral m mod (2 * numeral n))"
         by auto
     moreover from * divmod_digit_0 [of "numeral n" "numeral m"]
@@ -873,10 +701,10 @@
     ultimately show ?thesis by (simp only: divmod_def)
   qed
   then have "divmod m n =
-    divmod_step n (numeral m div numeral (Num.Bit0 n),
+    divmod_step (numeral n) (numeral m div numeral (Num.Bit0 n),
       numeral m mod numeral (Num.Bit0 n))"
     by (simp only: numeral.simps distrib mult_1)
-  then have "divmod m n = divmod_step n (divmod m (Num.Bit0 n))"
+  then have "divmod m n = divmod_step (numeral n) (divmod m (Num.Bit0 n))"
     by (simp add: divmod_def)
   with False show ?thesis by simp
 qed
@@ -910,12 +738,12 @@
 lemma divmod_steps [simp]:
   "divmod (num.Bit0 m) (num.Bit1 n) =
       (if m \<le> n then (0, numeral (num.Bit0 m))
-       else divmod_step (num.Bit1 n)
+       else divmod_step (numeral (num.Bit1 n))
              (divmod (num.Bit0 m)
                (num.Bit0 (num.Bit1 n))))"
   "divmod (num.Bit1 m) (num.Bit1 n) =
       (if m < n then (0, numeral (num.Bit1 m))
-       else divmod_step (num.Bit1 n)
+       else divmod_step (numeral (num.Bit1 n))
              (divmod (num.Bit1 m)
                (num.Bit0 (num.Bit1 n))))"
   by (simp_all add: divmod_divmod_step)
@@ -996,10 +824,10 @@
 where
   divmod'_nat_def: "divmod_nat m n = (numeral m div numeral n, numeral m mod numeral n)"
 
-definition divmod_step_nat :: "num \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat"
+definition divmod_step_nat :: "nat \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat"
 where
   "divmod_step_nat l qr = (let (q, r) = qr
-    in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
+    in if r \<ge> l then (2 * q + 1, r - l)
     else (2 * q, r))"
 
 instance by standard
@@ -1026,10 +854,10 @@
 where
   "divmod_int m n = (numeral m div numeral n, numeral m mod numeral n)"
 
-definition divmod_step_int :: "num \<Rightarrow> int \<times> int \<Rightarrow> int \<times> int"
+definition divmod_step_int :: "int \<Rightarrow> int \<times> int \<Rightarrow> int \<times> int"
 where
   "divmod_step_int l qr = (let (q, r) = qr
-    in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
+    in if r \<ge> l then (2 * q + 1, r - l)
     else (2 * q, r))"
 
 instance
@@ -1051,9 +879,9 @@
   "adjust_div (q, r) = q + of_bool (r \<noteq> 0)"
   by (simp add: adjust_div_def)
 
-qualified definition adjust_mod :: "int \<Rightarrow> int \<Rightarrow> int"
+qualified definition adjust_mod :: "num \<Rightarrow> int \<Rightarrow> int"
 where
-  [simp]: "adjust_mod l r = (if r = 0 then 0 else l - r)"
+  [simp]: "adjust_mod l r = (if r = 0 then 0 else numeral l - r)"
 
 lemma minus_numeral_div_numeral [simp]:
   "- numeral m div numeral n = - (adjust_div (divmod m n) :: int)"
@@ -1065,7 +893,7 @@
 qed
 
 lemma minus_numeral_mod_numeral [simp]:
-  "- numeral m mod numeral n = adjust_mod (numeral n) (snd (divmod m n) :: int)"
+  "- numeral m mod numeral n = adjust_mod n (snd (divmod m n) :: int)"
 proof (cases "snd (divmod m n) = (0::int)")
   case True
   then show ?thesis
@@ -1089,7 +917,7 @@
 qed
   
 lemma numeral_mod_minus_numeral [simp]:
-  "numeral m mod - numeral n = - adjust_mod (numeral n) (snd (divmod m n) :: int)"
+  "numeral m mod - numeral n = - adjust_mod n (snd (divmod m n) :: int)"
 proof (cases "snd (divmod m n) = (0::int)")
   case True
   then show ?thesis
@@ -1108,7 +936,7 @@
   using minus_numeral_div_numeral [of Num.One n] by simp  
 
 lemma minus_one_mod_numeral [simp]:
-  "- 1 mod numeral n = adjust_mod (numeral n) (snd (divmod Num.One n) :: int)"
+  "- 1 mod numeral n = adjust_mod n (snd (divmod Num.One n) :: int)"
   using minus_numeral_mod_numeral [of Num.One n] by simp
 
 lemma one_div_minus_numeral [simp]:
@@ -1116,7 +944,7 @@
   using numeral_div_minus_numeral [of Num.One n] by simp
   
 lemma one_mod_minus_numeral [simp]:
-  "1 mod - numeral n = - adjust_mod (numeral n) (snd (divmod Num.One n) :: int)"
+  "1 mod - numeral n = - adjust_mod n (snd (divmod Num.One n) :: int)"
   using numeral_mod_minus_numeral [of Num.One n] by simp
 
 end
@@ -1225,9 +1053,9 @@
     "Int.Pos m div Int.Pos n = (fst (divmod m n) :: int)"
     "Int.Pos m mod Int.Pos n = (snd (divmod m n) :: int)"
     "Int.Neg m div Int.Pos n = - (Divides.adjust_div (divmod m n) :: int)"
-    "Int.Neg m mod Int.Pos n = Divides.adjust_mod (Int.Pos n) (snd (divmod m n) :: int)"
+    "Int.Neg m mod Int.Pos n = Divides.adjust_mod n (snd (divmod m n) :: int)"
     "Int.Pos m div Int.Neg n = - (Divides.adjust_div (divmod m n) :: int)"
-    "Int.Pos m mod Int.Neg n = - Divides.adjust_mod (Int.Pos n) (snd (divmod m n) :: int)"
+    "Int.Pos m mod Int.Neg n = - Divides.adjust_mod n (snd (divmod m n) :: int)"
     "Int.Neg m div Int.Neg n = (fst (divmod m n) :: int)"
     "Int.Neg m mod Int.Neg n = - (snd (divmod m n) :: int)"
   by simp_all

--- a/src/HOL/Euclidean_Division.thy	Sat Aug 20 21:33:51 2022 +0200
+++ b/src/HOL/Euclidean_Division.thy	Sat Aug 20 21:34:55 2022 +0200
@@ -321,7 +321,7 @@
 
 lemma div_plus_div_distrib_dvd_left:
   "c dvd a \<Longrightarrow> (a + b) div c = a div c + b div c"
-  by (cases "c = 0") (auto elim: dvdE)
+  by (cases "c = 0") auto
 
 lemma div_plus_div_distrib_dvd_right:
   "c dvd b \<Longrightarrow> (a + b) div c = a div c + b div c"
@@ -603,7 +603,7 @@
 
   
 subsection \<open>Uniquely determined division\<close>
-  
+
 class unique_euclidean_semiring = euclidean_semiring + 
   assumes euclidean_size_mult: "euclidean_size (a * b) = euclidean_size a * euclidean_size b"
   fixes division_segment :: "'a \<Rightarrow> 'a"
@@ -937,6 +937,14 @@
 
 end
 
+lemma div_nat_eqI:
+  "m div n = q" if "n * q \<le> m" and "m < n * Suc q" for m n q :: nat
+  by (rule div_eqI [of _ "m - n * q"]) (use that in \<open>simp_all add: algebra_simps\<close>)
+
+lemma mod_nat_eqI:
+  "m mod n = r" if "r < n" and "r \<le> m" and "n dvd m - r" for m n r :: nat
+  by (rule mod_eqI [of _ _ "(m - r) div n"]) (use that in \<open>simp_all add: algebra_simps\<close>)
+
 text \<open>Tool support\<close>
 
 ML \<open>
@@ -967,14 +975,6 @@
 simproc_setup cancel_div_mod_nat ("(m::nat) + n") =
   \<open>K Cancel_Div_Mod_Nat.proc\<close>
 
-lemma div_nat_eqI:
-  "m div n = q" if "n * q \<le> m" and "m < n * Suc q" for m n q :: nat
-  by (rule div_eqI [of _ "m - n * q"]) (use that in \<open>simp_all add: algebra_simps\<close>)
-
-lemma mod_nat_eqI:
-  "m mod n = r" if "r < n" and "r \<le> m" and "n dvd m - r" for m n r :: nat
-  by (rule mod_eqI [of _ _ "(m - r) div n"]) (use that in \<open>simp_all add: algebra_simps\<close>)
-
 lemma div_mult_self_is_m [simp]:
   "m * n div n = m" if "n > 0" for m n :: nat
   using that by simp
@@ -1030,6 +1030,41 @@
   and mod_less [simp]: "m mod n = m"
   if "m < n" for m n :: nat
   using that by (auto intro: div_eqI mod_eqI) 
+ 
+lemma split_div:
+  \<open>P (m div n) \<longleftrightarrow>
+    (n = 0 \<longrightarrow> P 0) \<and>
+    (n \<noteq> 0 \<longrightarrow> (\<forall>i j. j < n \<and> m = n * i + j \<longrightarrow> P i))\<close> (is ?div)
+  and split_mod:
+  \<open>Q (m mod n) \<longleftrightarrow>
+    (n = 0 \<longrightarrow> Q m) \<and>
+    (n \<noteq> 0 \<longrightarrow> (\<forall>i j. j < n \<and> m = n * i + j \<longrightarrow> Q j))\<close> (is ?mod)
+  for m n :: nat
+proof -
+  have *: \<open>R (m div n) (m mod n) \<longleftrightarrow>
+    (n = 0 \<longrightarrow> R 0 m) \<and>
+    (n \<noteq> 0 \<longrightarrow> (\<forall>i j. j < n \<and> m = n * i + j \<longrightarrow> R i j))\<close> for R
+    by (cases \<open>n = 0\<close>) auto
+  from * [of \<open>\<lambda>q _. P q\<close>] show ?div .
+  from * [of \<open>\<lambda>_ r. Q r\<close>] show ?mod .
+qed
+
+declare split_div [of _ _ \<open>numeral n\<close>, linarith_split] for n
+declare split_mod [of _ _ \<open>numeral n\<close>, linarith_split] for n
+
+lemma split_div':
+  "P (m div n) \<longleftrightarrow> n = 0 \<and> P 0 \<or> (\<exists>q. (n * q \<le> m \<and> m < n * Suc q) \<and> P q)"
+proof (cases "n = 0")
+  case True
+  then show ?thesis
+    by simp
+next
+  case False
+  then have "n * q \<le> m \<and> m < n * Suc q \<longleftrightarrow> m div n = q" for q
+    by (auto intro: div_nat_eqI dividend_less_times_div)
+  then show ?thesis
+    by auto
+qed
 
 lemma le_div_geq:
   "m div n = Suc ((m - n) div n)" if "0 < n" and "n \<le> m" for m n :: nat
@@ -1418,68 +1453,6 @@
     by simp
 qed
 
-lemma split_div:
-  "P (m div n) \<longleftrightarrow> (n = 0 \<longrightarrow> P 0) \<and> (n \<noteq> 0 \<longrightarrow>
-     (\<forall>i j. j < n \<longrightarrow> m = n * i + j \<longrightarrow> P i))"
-     (is "?P = ?Q") for m n :: nat
-proof (cases "n = 0")
-  case True
-  then show ?thesis
-    by simp
-next
-  case False
-  show ?thesis
-  proof
-    assume ?P
-    with False show ?Q
-      by auto
-  next
-    assume ?Q
-    with False have *: "\<And>i j. j < n \<Longrightarrow> m = n * i + j \<Longrightarrow> P i"
-      by simp
-    with False show ?P
-      by (auto intro: * [of "m mod n"])
-  qed
-qed
-
-lemma split_div':
-  "P (m div n) \<longleftrightarrow> n = 0 \<and> P 0 \<or> (\<exists>q. (n * q \<le> m \<and> m < n * Suc q) \<and> P q)"
-proof (cases "n = 0")
-  case True
-  then show ?thesis
-    by simp
-next
-  case False
-  then have "n * q \<le> m \<and> m < n * Suc q \<longleftrightarrow> m div n = q" for q
-    by (auto intro: div_nat_eqI dividend_less_times_div)
-  then show ?thesis
-    by auto
-qed
-
-lemma split_mod:
-  "P (m mod n) \<longleftrightarrow> (n = 0 \<longrightarrow> P m) \<and> (n \<noteq> 0 \<longrightarrow>
-     (\<forall>i j. j < n \<longrightarrow> m = n * i + j \<longrightarrow> P j))"
-     (is "?P \<longleftrightarrow> ?Q") for m n :: nat
-proof (cases "n = 0")
-  case True
-  then show ?thesis
-    by simp
-next
-  case False
-  show ?thesis
-  proof
-    assume ?P
-    with False show ?Q
-      by auto
-  next
-    assume ?Q
-    with False have *: "\<And>i j. j < n \<Longrightarrow> m = n * i + j \<Longrightarrow> P j"
-      by simp
-    with False show ?P
-      by (auto intro: * [of _ "m div n"])
-  qed
-qed
-
 lemma funpow_mod_eq: \<^marker>\<open>contributor \<open>Lars Noschinski\<close>\<close>
   \<open>(f ^^ (m mod n)) x = (f ^^ m) x\<close> if \<open>(f ^^ n) x = x\<close>
 proof -
@@ -1494,31 +1467,35 @@
 qed
 
 
-subsection \<open>Euclidean division on \<^typ>\<open>int\<close>\<close>
+subsection \<open>Elementary euclidean division on \<^typ>\<open>int\<close>\<close>
 
-instantiation int :: normalization_semidom
+subsubsection \<open>Basic instantiation\<close>
+
+instantiation int :: "{normalization_semidom, idom_modulo}"
 begin
 
-definition normalize_int :: "int \<Rightarrow> int"
-  where [simp]: "normalize = (abs :: int \<Rightarrow> int)"
-
-definition unit_factor_int :: "int \<Rightarrow> int"
-  where [simp]: "unit_factor = (sgn :: int \<Rightarrow> int)"
+definition normalize_int :: \<open>int \<Rightarrow> int\<close>
+  where [simp]: \<open>normalize = (abs :: int \<Rightarrow> int)\<close>
 
-definition divide_int :: "int \<Rightarrow> int \<Rightarrow> int"
-  where "k div l = (if l = 0 then 0
-    else if sgn k = sgn l
-      then int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)
-      else - int (nat \<bar>k\<bar> div nat \<bar>l\<bar> + of_bool (\<not> l dvd k)))"
+definition unit_factor_int :: \<open>int \<Rightarrow> int\<close>
+  where [simp]: \<open>unit_factor = (sgn :: int \<Rightarrow> int)\<close>
+
+definition divide_int :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close>
+  where \<open>k div l = (sgn k * sgn l * int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)
+    - of_bool (l \<noteq> 0 \<and> sgn k \<noteq> sgn l \<and> \<not> l dvd k))\<close>
 
 lemma divide_int_unfold:
-  "(sgn k * int m) div (sgn l * int n) =
-   (if sgn l = 0 \<or> sgn k = 0 \<or> n = 0 then 0
-    else if sgn k = sgn l
-      then int (m div n)
-      else - int (m div n + of_bool (\<not> n dvd m)))"
-  by (auto simp add: divide_int_def sgn_0_0 sgn_1_pos sgn_mult abs_mult
-    nat_mult_distrib)
+  \<open>(sgn k * int m) div (sgn l * int n) = (sgn k * sgn l * int (m div n)
+    - of_bool ((k = 0 \<longleftrightarrow> m = 0) \<and> l \<noteq> 0 \<and> n \<noteq> 0 \<and> sgn k \<noteq> sgn l \<and> \<not> n dvd m))\<close>
+  by (simp add: divide_int_def sgn_mult nat_mult_distrib abs_mult sgn_eq_0_iff ac_simps)
+
+definition modulo_int :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close>
+  where \<open>k mod l = sgn k * int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>) + l * of_bool (sgn k \<noteq> sgn l \<and> \<not> l dvd k)\<close>
+
+lemma modulo_int_unfold:
+  \<open>(sgn k * int m) mod (sgn l * int n) =
+    sgn k * int (m mod (of_bool (l \<noteq> 0) * n)) + (sgn l * int n) * of_bool ((k = 0 \<longleftrightarrow> m = 0) \<and> sgn k \<noteq> sgn l \<and> \<not> n dvd m)\<close>
+  by (auto simp add: modulo_int_def sgn_mult abs_mult)
 
 instance proof
   fix k :: int show "k div 0 = 0"
@@ -1533,10 +1510,19 @@
   with k l \<open>l \<noteq> 0\<close> show "k * l div l = k"
     by (simp only: divide_int_unfold)
       (auto simp add: algebra_simps sgn_mult sgn_1_pos sgn_0_0)
+next
+  fix k l :: int
+  obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m" 
+    by (blast intro: int_sgnE elim: that)
+  then show "k div l * l + k mod l = k"
+    by (simp add: divide_int_unfold modulo_int_unfold algebra_simps modulo_nat_def of_nat_diff)
 qed (auto simp add: sgn_mult mult_sgn_abs abs_eq_iff')
 
 end
 
+
+subsubsection \<open>Algebraic foundations\<close>
+
 lemma coprime_int_iff [simp]:
   "coprime (int m) (int n) \<longleftrightarrow> coprime m n" (is "?P \<longleftrightarrow> ?Q")
 proof
@@ -1595,36 +1581,66 @@
   for a b :: int
   by (drule coprime_common_divisor [of _ _ x]) simp_all
 
-instantiation int :: idom_modulo
-begin
+
+subsubsection \<open>Basic conversions\<close>
+
+lemma div_abs_eq_div_nat:
+  "\<bar>k\<bar> div \<bar>l\<bar> = int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)"
+  by (auto simp add: divide_int_def)
+
+lemma div_eq_div_abs:
+  \<open>k div l = sgn k * sgn l * (\<bar>k\<bar> div \<bar>l\<bar>)
+    - of_bool (l \<noteq> 0 \<and> sgn k \<noteq> sgn l \<and> \<not> l dvd k)\<close>
+  for k l :: int
+  by (simp add: divide_int_def [of k l] div_abs_eq_div_nat)
 
-definition modulo_int :: "int \<Rightarrow> int \<Rightarrow> int"
-  where "k mod l = (if l = 0 then k
-    else if sgn k = sgn l
-      then sgn l * int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)
-      else sgn l * (\<bar>l\<bar> * of_bool (\<not> l dvd k) - int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)))"
+lemma div_abs_eq:
+  \<open>\<bar>k\<bar> div \<bar>l\<bar> = sgn k * sgn l * (k div l + of_bool (sgn k \<noteq> sgn l \<and> \<not> l dvd k))\<close>
+  for k l :: int
+  by (simp add: div_eq_div_abs [of k l] ac_simps)
+
+lemma mod_abs_eq_div_nat:
+  "\<bar>k\<bar> mod \<bar>l\<bar> = int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)"
+  by (simp add: modulo_int_def)
+
+lemma mod_eq_mod_abs:
+  \<open>k mod l = sgn k * (\<bar>k\<bar> mod \<bar>l\<bar>) + l * of_bool (sgn k \<noteq> sgn l \<and> \<not> l dvd k)\<close>
+  for k l :: int
+  by (simp add: modulo_int_def [of k l] mod_abs_eq_div_nat)
 
-lemma modulo_int_unfold:
-  "(sgn k * int m) mod (sgn l * int n) =
-   (if sgn l = 0 \<or> sgn k = 0 \<or> n = 0 then sgn k * int m
-    else if sgn k = sgn l
-      then sgn l * int (m mod n)
-      else sgn l * (int (n * of_bool (\<not> n dvd m)) - int (m mod n)))"
-  by (auto simp add: modulo_int_def sgn_0_0 sgn_1_pos sgn_mult abs_mult
-    nat_mult_distrib)
+lemma mod_abs_eq:
+  \<open>\<bar>k\<bar> mod \<bar>l\<bar> = sgn k * (k mod l - l * of_bool (sgn k \<noteq> sgn l \<and> \<not> l dvd k))\<close>
+  for k l :: int
+  by (auto simp: mod_eq_mod_abs [of k l])
+
+lemma div_sgn_abs_cancel:
+  fixes k l v :: int
+  assumes "v \<noteq> 0"
+  shows "(sgn v * \<bar>k\<bar>) div (sgn v * \<bar>l\<bar>) = \<bar>k\<bar> div \<bar>l\<bar>"
+  using assms by (simp add: sgn_mult abs_mult sgn_0_0
+    divide_int_def [of "sgn v * \<bar>k\<bar>" "sgn v * \<bar>l\<bar>"] flip: div_abs_eq_div_nat)
 
-instance proof
-  fix k l :: int
-  obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m" 
-    by (blast intro: int_sgnE elim: that)
-  then show "k div l * l + k mod l = k"
-    by (auto simp add: divide_int_unfold modulo_int_unfold algebra_simps dest!: sgn_not_eq_imp)
-       (simp_all add: of_nat_mult [symmetric] of_nat_add [symmetric]
-         distrib_left [symmetric] minus_mult_right
-         del: of_nat_mult minus_mult_right [symmetric])
-qed
+lemma div_eq_sgn_abs:
+  fixes k l v :: int
+  assumes "sgn k = sgn l"
+  shows "k div l = \<bar>k\<bar> div \<bar>l\<bar>"
+  using assms by (auto simp add: div_abs_eq)
 
-end
+lemma div_dvd_sgn_abs:
+  fixes k l :: int
+  assumes "l dvd k"
+  shows "k div l = (sgn k * sgn l) * (\<bar>k\<bar> div \<bar>l\<bar>)"
+  using assms by (auto simp add: div_abs_eq ac_simps)
+
+lemma div_noneq_sgn_abs:
+  fixes k l :: int
+  assumes "l \<noteq> 0"
+  assumes "sgn k \<noteq> sgn l"
+  shows "k div l = - (\<bar>k\<bar> div \<bar>l\<bar>) - of_bool (\<not> l dvd k)"
+  using assms by (auto simp add: div_abs_eq ac_simps sgn_0_0 dest!: sgn_not_eq_imp)
+
+
+subsubsection \<open>Euclidean division\<close>
 
 instantiation int :: unique_euclidean_ring
 begin
@@ -1649,8 +1665,9 @@
   obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m" 
     by (blast intro: int_sgnE elim: that)
   with that show ?thesis
-    by (simp add: modulo_int_unfold sgn_0_0 sgn_1_pos sgn_1_neg
-      abs_mult mod_greater_zero_iff_not_dvd)
+    by (auto simp add: modulo_int_unfold abs_mult mod_greater_zero_iff_not_dvd
+        simp flip: right_diff_distrib dest!: sgn_not_eq_imp)
+      (simp add: sgn_0_0)
 qed
 
 lemma sgn_mod:
@@ -1659,8 +1676,8 @@
   obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m" 
     by (blast intro: int_sgnE elim: that)
   with that show ?thesis
-    by (simp add: modulo_int_unfold sgn_0_0 sgn_1_pos sgn_1_neg sgn_mult)
-      (simp add: dvd_eq_mod_eq_0)
+    by (auto simp add: modulo_int_unfold sgn_mult mod_greater_zero_iff_not_dvd
+      simp flip: right_diff_distrib dest!: sgn_not_eq_imp)
 qed
 
 instance proof
@@ -1700,8 +1717,8 @@
       from \<open>r = 0\<close> have *: "q * l + r = sgn (t * s) * int (n * m)"
         using q l by (simp add: ac_simps sgn_mult)
       from \<open>s \<noteq> 0\<close> \<open>n > 0\<close> show ?thesis
-        by (simp only: *, simp only: q l divide_int_unfold)
-          (auto simp add: sgn_mult sgn_0_0 sgn_1_pos)
+        by (simp only: *, simp only: * q l divide_int_unfold)
+          (auto simp add: sgn_mult ac_simps)
     qed
   next
     case False
@@ -1728,123 +1745,6 @@
 
 end
 
-lemma pos_mod_bound [simp]:
-  "k mod l < l" if "l > 0" for k l :: int
-proof -
-  obtain m and s where "k = sgn s * int m"
-    by (rule int_sgnE)
-  moreover from that obtain n where "l = sgn 1 * int n"
-    by (cases l) simp_all
-  moreover from this that have "n > 0"
-    by simp
-  ultimately show ?thesis
-    by (simp only: modulo_int_unfold)
-      (simp add: mod_greater_zero_iff_not_dvd)
-qed
-
-lemma neg_mod_bound [simp]:
-  "l < k mod l" if "l < 0" for k l :: int
-proof -
-  obtain m and s where "k = sgn s * int m"
-    by (rule int_sgnE)
-  moreover from that obtain q where "l = sgn (- 1) * int (Suc q)"
-    by (cases l) simp_all
-  moreover define n where "n = Suc q"
-  then have "Suc q = n"
-    by simp
-  ultimately show ?thesis
-    by (simp only: modulo_int_unfold)
-      (simp add: mod_greater_zero_iff_not_dvd)
-qed
-
-lemma pos_mod_sign [simp]:
-  "0 \<le> k mod l" if "l > 0" for k l :: int
-proof -
-  obtain m and s where "k = sgn s * int m"
-    by (rule int_sgnE)
-  moreover from that obtain n where "l = sgn 1 * int n"
-    by (cases l) auto
-  moreover from this that have "n > 0"
-    by simp
-  ultimately show ?thesis
-    by (simp only: modulo_int_unfold) simp
-qed
-
-lemma neg_mod_sign [simp]:
-  "k mod l \<le> 0" if "l < 0" for k l :: int
-proof -
-  obtain m and s where "k = sgn s * int m"
-    by (rule int_sgnE)
-  moreover from that obtain q where "l = sgn (- 1) * int (Suc q)"
-    by (cases l) simp_all
-  moreover define n where "n = Suc q"
-  then have "Suc q = n"
-    by simp
-  ultimately show ?thesis
-    by (simp only: modulo_int_unfold) simp
-qed
-
-lemma div_pos_pos_trivial [simp]:
-  "k div l = 0" if "k \<ge> 0" and "k < l" for k l :: int
-  using that by (simp add: unique_euclidean_semiring_class.div_eq_0_iff division_segment_int_def)
-
-lemma mod_pos_pos_trivial [simp]:
-  "k mod l = k" if "k \<ge> 0" and "k < l" for k l :: int
-  using that by (simp add: mod_eq_self_iff_div_eq_0)
-
-lemma div_neg_neg_trivial [simp]:
-  "k div l = 0" if "k \<le> 0" and "l < k" for k l :: int
-  using that by (cases "k = 0") (simp, simp add: unique_euclidean_semiring_class.div_eq_0_iff division_segment_int_def)
-
-lemma mod_neg_neg_trivial [simp]:
-  "k mod l = k" if "k \<le> 0" and "l < k" for k l :: int
-  using that by (simp add: mod_eq_self_iff_div_eq_0)
-
-lemma div_pos_neg_trivial:
-  "k div l = - 1" if "0 < k" and "k + l \<le> 0" for k l :: int
-proof (cases \<open>l = - k\<close>)
-  case True
-  with that show ?thesis
-    by (simp add: divide_int_def)
-next
-  case False
-  show ?thesis
-    apply (rule div_eqI [of _ "k + l"])
-    using False that apply (simp_all add: division_segment_int_def)
-    done
-qed
-
-lemma mod_pos_neg_trivial:
-  "k mod l = k + l" if "0 < k" and "k + l \<le> 0" for k l :: int
-proof (cases \<open>l = - k\<close>)
-  case True
-  with that show ?thesis
-    by (simp add: divide_int_def)
-next
-  case False
-  show ?thesis
-    apply (rule mod_eqI [of _ _ \<open>- 1\<close>])
-    using False that apply (simp_all add: division_segment_int_def)
-    done
-qed
-
-text \<open>There is neither \<open>div_neg_pos_trivial\<close> nor \<open>mod_neg_pos_trivial\<close>
-  because \<^term>\<open>0 div l = 0\<close> would supersede it.\<close>
-
-text \<open>Distributive laws for function \<open>nat\<close>.\<close>
-
-lemma nat_div_distrib:
-  \<open>nat (x div y) = nat x div nat y\<close> if \<open>0 \<le> x\<close>
-  using that by (simp add: divide_int_def sgn_if)
-
-lemma nat_div_distrib':
-  \<open>nat (x div y) = nat x div nat y\<close> if \<open>0 \<le> y\<close>
-  using that by (simp add: divide_int_def sgn_if)
-
-lemma nat_mod_distrib: \<comment> \<open>Fails if y<0: the LHS collapses to (nat z) but the RHS doesn't\<close>
-  \<open>nat (x mod y) = nat x mod nat y\<close> if \<open>0 \<le> x\<close> \<open>0 \<le> y\<close>
-  using that by (simp add: modulo_int_def sgn_if)
-
 
 subsection \<open>Special case: euclidean rings containing the natural numbers\<close>
 
@@ -2075,7 +1975,7 @@
   proof (cases \<open>n \<le> m\<close>)
     case True
     then show ?thesis
-      by (simp add: Suc_le_lessD min.absorb2)
+      by (simp add: Suc_le_lessD)
   next
     case False
     then have \<open>m < n\<close>
@@ -2109,7 +2009,218 @@
   by standard (simp_all add: dvd_eq_mod_eq_0)
 
 instance int :: unique_euclidean_ring_with_nat
-  by standard (simp_all add: dvd_eq_mod_eq_0 divide_int_def division_segment_int_def)
+  by standard (auto simp add: divide_int_def division_segment_int_def elim: contrapos_np)
+
+
+subsection \<open>More on euclidean division on \<^typ>\<open>int\<close>\<close>
+
+subsubsection \<open>Trivial reduction steps\<close>
+
+lemma div_pos_pos_trivial [simp]:
+  "k div l = 0" if "k \<ge> 0" and "k < l" for k l :: int
+  using that by (simp add: unique_euclidean_semiring_class.div_eq_0_iff division_segment_int_def)
+
+lemma mod_pos_pos_trivial [simp]:
+  "k mod l = k" if "k \<ge> 0" and "k < l" for k l :: int
+  using that by (simp add: mod_eq_self_iff_div_eq_0)
+
+lemma div_neg_neg_trivial [simp]:
+  "k div l = 0" if "k \<le> 0" and "l < k" for k l :: int
+  using that by (cases "k = 0") (simp, simp add: unique_euclidean_semiring_class.div_eq_0_iff division_segment_int_def)
+
+lemma mod_neg_neg_trivial [simp]:
+  "k mod l = k" if "k \<le> 0" and "l < k" for k l :: int
+  using that by (simp add: mod_eq_self_iff_div_eq_0)
+
+lemma div_pos_neg_trivial:
+  "k div l = - 1" if "0 < k" and "k + l \<le> 0" for k l :: int
+proof (cases \<open>l = - k\<close>)
+  case True
+  with that show ?thesis
+    by (simp add: divide_int_def)
+next
+  case False
+  show ?thesis
+    apply (rule div_eqI [of _ "k + l"])
+    using False that apply (simp_all add: division_segment_int_def)
+    done
+qed
+
+lemma mod_pos_neg_trivial:
+  "k mod l = k + l" if "0 < k" and "k + l \<le> 0" for k l :: int
+proof (cases \<open>l = - k\<close>)
+  case True
+  with that show ?thesis
+    by (simp add: divide_int_def)
+next
+  case False
+  show ?thesis
+    apply (rule mod_eqI [of _ _ \<open>- 1\<close>])
+    using False that apply (simp_all add: division_segment_int_def)
+    done
+qed
+
+text \<open>There is neither \<open>div_neg_pos_trivial\<close> nor \<open>mod_neg_pos_trivial\<close>
+  because \<^term>\<open>0 div l = 0\<close> would supersede it.\<close>
+
+
+subsubsection \<open>Laws for unary minus\<close>
+
+lemma zmod_zminus1_not_zero:
+  fixes k l :: int
+  shows "- k mod l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
+  by (simp add: mod_eq_0_iff_dvd)
+
+lemma zmod_zminus2_not_zero:
+  fixes k l :: int
+  shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
+  by (simp add: mod_eq_0_iff_dvd)
+
+lemma zdiv_zminus1_eq_if:
+  \<open>(- a) div b = (if a mod b = 0 then - (a div b) else - (a div b) - 1)\<close>
+  if \<open>b \<noteq> 0\<close> for a b :: int
+  using that sgn_not_eq_imp [of b \<open>- a\<close>]
+  by (cases \<open>a = 0\<close>) (auto simp add: div_eq_div_abs [of \<open>- a\<close> b] div_eq_div_abs [of a b] sgn_eq_0_iff)
+
+lemma zdiv_zminus2_eq_if:
+  \<open>a div (- b) = (if a mod b = 0 then - (a div b) else - (a div b) - 1)\<close>
+  if \<open>b \<noteq> 0\<close> for a b :: int
+  using that by (auto simp add: zdiv_zminus1_eq_if div_minus_right)
+
+lemma zmod_zminus1_eq_if:
+  \<open>(- a) mod b = (if a mod b = 0 then 0 else b - (a mod b))\<close>
+  for a b :: int
+  by (cases \<open>b = 0\<close>)
+    (auto simp flip: minus_div_mult_eq_mod simp add: zdiv_zminus1_eq_if algebra_simps)
+
+lemma zmod_zminus2_eq_if:
+  \<open>a mod (- b) = (if a mod b = 0 then 0 else (a mod b) - b)\<close>
+  for a b :: int
+  by (auto simp add: zmod_zminus1_eq_if mod_minus_right)
+
+
+subsubsection \<open>Borders\<close>
+
+lemma pos_mod_bound [simp]:
+  "k mod l < l" if "l > 0" for k l :: int
+proof -
+  obtain m and s where "k = sgn s * int m"
+    by (rule int_sgnE)
+  moreover from that obtain n where "l = sgn 1 * int n"
+    by (cases l) simp_all
+  moreover from this that have "n > 0"
+    by simp
+  ultimately show ?thesis
+    by (simp only: modulo_int_unfold)
+      (auto simp add: mod_greater_zero_iff_not_dvd sgn_1_pos)
+qed
+
+lemma neg_mod_bound [simp]:
+  "l < k mod l" if "l < 0" for k l :: int
+proof -
+  obtain m and s where "k = sgn s * int m"
+    by (rule int_sgnE)
+  moreover from that obtain q where "l = sgn (- 1) * int (Suc q)"
+    by (cases l) simp_all
+  moreover define n where "n = Suc q"
+  then have "Suc q = n"
+    by simp
+  ultimately show ?thesis
+    by (simp only: modulo_int_unfold)
+      (auto simp add: mod_greater_zero_iff_not_dvd sgn_1_neg)
+qed
+
+lemma pos_mod_sign [simp]:
+  "0 \<le> k mod l" if "l > 0" for k l :: int
+proof -
+  obtain m and s where "k = sgn s * int m"
+    by (rule int_sgnE)
+  moreover from that obtain n where "l = sgn 1 * int n"
+    by (cases l) auto
+  moreover from this that have "n > 0"
+    by simp
+  ultimately show ?thesis
+    by (simp only: modulo_int_unfold) (auto simp add: sgn_1_pos)
+qed
+
+lemma neg_mod_sign [simp]:
+  "k mod l \<le> 0" if "l < 0" for k l :: int
+proof -
+  obtain m and s where "k = sgn s * int m"
+    by (rule int_sgnE)
+  moreover from that obtain q where "l = sgn (- 1) * int (Suc q)"
+    by (cases l) simp_all
+  moreover define n where "n = Suc q"
+  then have "Suc q = n"
+    by simp
+  moreover have \<open>int (m mod n) \<le> int n\<close>
+    using \<open>Suc q = n\<close> by simp
+  then have \<open>sgn s * int (m mod n) \<le> int n\<close>
+    by (cases s \<open>0::int\<close> rule: linorder_cases) simp_all
+  ultimately show ?thesis
+    by (simp only: modulo_int_unfold) auto
+qed
+
+
+subsubsection \<open>Splitting Rules for div and mod\<close>
+
+lemma split_zdiv:
+  \<open>P (n div k) \<longleftrightarrow>
+    (k = 0 \<longrightarrow> P 0) \<and>
+    (0 < k \<longrightarrow> (\<forall>i j. 0 \<le> j \<and> j < k \<and> n = k * i + j \<longrightarrow> P i)) \<and>
+    (k < 0 \<longrightarrow> (\<forall>i j. k < j \<and> j \<le> 0 \<and> n = k * i + j \<longrightarrow> P i))\<close> (is ?div)
+  and split_zmod:
+  \<open>Q (n mod k) \<longleftrightarrow>
+    (k = 0 \<longrightarrow> Q n) \<and>
+    (0 < k \<longrightarrow> (\<forall>i j. 0 \<le> j \<and> j < k \<and> n = k * i + j \<longrightarrow> Q j)) \<and>
+    (k < 0 \<longrightarrow> (\<forall>i j. k < j \<and> j \<le> 0 \<and> n = k * i + j \<longrightarrow> Q j))\<close> (is ?mod)
+  for n k :: int
+proof -
+  have *: \<open>R (n div k) (n mod k) \<longleftrightarrow>
+    (k = 0 \<longrightarrow> R 0 n) \<and>
+    (0 < k \<longrightarrow> (\<forall>i j. 0 \<le> j \<and> j < k \<and> n = k * i + j \<longrightarrow> R i j)) \<and>
+    (k < 0 \<longrightarrow> (\<forall>i j. k < j \<and> j \<le> 0 \<and> n = k * i + j \<longrightarrow> R i j))\<close> for R
+    by (cases \<open>k = 0\<close>)
+      (auto simp add: linorder_class.neq_iff)
+  from * [of \<open>\<lambda>q _. P q\<close>] show ?div .
+  from * [of \<open>\<lambda>_ r. Q r\<close>] show ?mod .
+qed
+ 
+text \<open>Enable (lin)arith to deal with \<^const>\<open>divide\<close> and \<^const>\<open>modulo\<close>
+  when these are applied to some constant that is of the form
+  \<^term>\<open>numeral k\<close>:\<close>
+declare split_zdiv [of _ _ \<open>numeral n\<close>, linarith_split] for n
+declare split_zdiv [of _ _ \<open>- numeral n\<close>, linarith_split] for n
+declare split_zmod [of _ _ \<open>numeral n\<close>, linarith_split] for n
+declare split_zmod [of _ _ \<open>- numeral n\<close>, linarith_split] for n
+
+lemma zdiv_eq_0_iff:
+  "i div k = 0 \<longleftrightarrow> k = 0 \<or> 0 \<le> i \<and> i < k \<or> i \<le> 0 \<and> k < i" (is "?L = ?R")
+  for i k :: int
+proof
+  assume ?L
+  moreover have "?L \<longrightarrow> ?R"
+    by (rule split_zdiv [THEN iffD2]) simp
+  ultimately show ?R
+    by blast
+next
+  assume ?R then show ?L
+    by auto
+qed
+
+lemma zmod_trivial_iff:
+  fixes i k :: int
+  shows "i mod k = i \<longleftrightarrow> k = 0 \<or> 0 \<le> i \<and> i < k \<or> i \<le> 0 \<and> k < i"
+proof -
+  have "i mod k = i \<longleftrightarrow> i div k = 0"
+    using div_mult_mod_eq [of i k] by safe auto
+  with zdiv_eq_0_iff
+  show ?thesis
+    by simp
+qed
+
+
+subsubsection \<open>Algebraic rewrites\<close>
 
 lemma zdiv_zmult2_eq:
   \<open>a div (b * c) = (a div b) div c\<close> if \<open>c \<ge> 0\<close> for a b c :: int
@@ -2123,6 +2234,18 @@
     using div_mult2_eq' [of \<open>- a\<close> \<open>nat (- b)\<close> \<open>nat c\<close>] by simp
 qed
 
+lemma zdiv_zmult2_eq':
+  \<open>k div (l * j) = ((sgn j * k) div l) div \<bar>j\<bar>\<close> for k l j :: int
+proof -
+  have \<open>k div (l * j) = (sgn j * k) div (sgn j * (l * j))\<close>
+    by (simp add: sgn_0_0)
+  also have \<open>sgn j * (l * j) = l * \<bar>j\<bar>\<close>
+    by (simp add: mult.left_commute [of _ l] abs_sgn) (simp add: ac_simps)
+  also have \<open>(sgn j * k) div (l * \<bar>j\<bar>) = ((sgn j * k) div l) div \<bar>j\<bar>\<close>
+    by (simp add: zdiv_zmult2_eq)
+  finally show ?thesis .
+qed
+
 lemma zmod_zmult2_eq:
   \<open>a mod (b * c) = b * (a div b mod c) + a mod b\<close> if \<open>c \<ge> 0\<close> for a b c :: int
 proof (cases \<open>b \<ge> 0\<close>)
@@ -2135,6 +2258,37 @@
     using mod_mult2_eq' [of \<open>- a\<close> \<open>nat (- b)\<close> \<open>nat c\<close>] by simp
 qed
 
+lemma half_nonnegative_int_iff [simp]:
+  \<open>k div 2 \<ge> 0 \<longleftrightarrow> k \<ge> 0\<close> for k :: int
+  by auto
+
+lemma half_negative_int_iff [simp]:
+  \<open>k div 2 < 0 \<longleftrightarrow> k < 0\<close> for k :: int
+  by auto
+
+
+subsubsection \<open>Distributive laws for conversions.\<close>
+
+lemma zdiv_int:
+  "int (a div b) = int a div int b"
+  by (fact of_nat_div)
+
+lemma zmod_int:
+  "int (a mod b) = int a mod int b"
+  by (fact of_nat_mod)
+
+lemma nat_div_distrib:
+  \<open>nat (x div y) = nat x div nat y\<close> if \<open>0 \<le> x\<close>
+  using that by (simp add: divide_int_def sgn_if)
+
+lemma nat_div_distrib':
+  \<open>nat (x div y) = nat x div nat y\<close> if \<open>0 \<le> y\<close>
+  using that by (simp add: divide_int_def sgn_if)
+
+lemma nat_mod_distrib: \<comment> \<open>Fails if y<0: the LHS collapses to (nat z) but the RHS doesn't\<close>
+  \<open>nat (x mod y) = nat x mod nat y\<close> if \<open>0 \<le> x\<close> \<open>0 \<le> y\<close>
+  using that by (simp add: modulo_int_def sgn_if)
+
 
 subsection \<open>Code generation\<close>
 

--- a/src/HOL/Fields.thy	Sat Aug 20 21:33:51 2022 +0200
+++ b/src/HOL/Fields.thy	Sat Aug 20 21:34:55 2022 +0200
@@ -13,32 +13,6 @@
 imports Nat
 begin
 
-context idom
-begin
-
-lemma inj_mult_left [simp]: \<open>inj ((*) a) \<longleftrightarrow> a \<noteq> 0\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
-proof
-  assume ?P
-  show ?Q
-  proof
-    assume \<open>a = 0\<close>
-    with \<open>?P\<close> have "inj ((*) 0)"
-      by simp
-    moreover have "0 * 0 = 0 * 1"
-      by simp
-    ultimately have "0 = 1"
-      by (rule injD)
-    then show False
-      by simp
-  qed
-next
-  assume ?Q then show ?P
-    by (auto intro: injI)
-qed
-
-end
-
-
 subsection \<open>Division rings\<close>
 
 text \<open>
@@ -60,7 +34,7 @@
 ML_file \<open>~~/src/Provers/Arith/fast_lin_arith.ML\<close>
 ML_file \<open>Tools/lin_arith.ML\<close>
 setup \<open>Lin_Arith.global_setup\<close>
-declaration \<open>K (
+declaration \<open>K (                 
   Lin_Arith.init_arith_data
   #> Lin_Arith.add_discrete_type \<^type_name>\<open>nat\<close>
   #> Lin_Arith.add_lessD @{thm Suc_leI}
@@ -85,7 +59,7 @@
    \<^text>\<open>fast_nat_arith_simproc\<close> anyway. However, it seems cheaper to activate the
    solver all the time rather than add the additional check.\<close>
 
-lemmas [arith_split] = nat_diff_split split_min split_max
+lemmas [linarith_split] = nat_diff_split split_min split_max abs_split
 
 text\<open>Lemmas \<open>divide_simps\<close> move division to the outside and eliminates them on (in)equalities.\<close>
 

--- a/src/HOL/Int.thy	Sat Aug 20 21:33:51 2022 +0200
+++ b/src/HOL/Int.thy	Sat Aug 20 21:34:55 2022 +0200
@@ -652,7 +652,7 @@
   "nat (of_bool P) = of_bool P"
   by auto
 
-lemma split_nat [arith_split]: "P (nat i) \<longleftrightarrow> ((\<forall>n. i = int n \<longrightarrow> P n) \<and> (i < 0 \<longrightarrow> P 0))"
+lemma split_nat [linarith_split]: "P (nat i) \<longleftrightarrow> ((\<forall>n. i = int n \<longrightarrow> P n) \<and> (i < 0 \<longrightarrow> P 0))"
   (is "?P = (?L \<and> ?R)")
   for i :: int
 proof (cases "i < 0")
@@ -737,16 +737,6 @@
 lemma zadd_int_left: "int m + (int n + z) = int (m + n) + z"
   by simp
 
-text \<open>
-  This version is proved for all ordered rings, not just integers!
-  It is proved here because attribute \<open>arith_split\<close> is not available
-  in theory \<open>Rings\<close>.
-  But is it really better than just rewriting with \<open>abs_if\<close>?
-\<close>
-lemma abs_split [arith_split, no_atp]: "P \<bar>a\<bar> \<longleftrightarrow> (0 \<le> a \<longrightarrow> P a) \<and> (a < 0 \<longrightarrow> P (- a))"
-  for a :: "'a::linordered_idom"
-  by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
-
 lemma negD:
   assumes "x < 0" shows "\<exists>n. x = - (int (Suc n))"
 proof -

--- a/src/HOL/Library/Signed_Division.thy	Sat Aug 20 21:33:51 2022 +0200
+++ b/src/HOL/Library/Signed_Division.thy	Sat Aug 20 21:34:55 2022 +0200
@@ -7,9 +7,41 @@
   imports Main
 begin
 
-class signed_division =
-  fixes signed_divide :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixl "sdiv" 70)
-  and signed_modulo :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixl "smod" 70)
+class signed_division = comm_semiring_1_cancel +
+  fixes signed_divide :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixl \<open>sdiv\<close> 70)
+  and signed_modulo :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixl \<open>smod\<close> 70)
+  assumes sdiv_mult_smod_eq: \<open>a sdiv b * b + a smod b = a\<close>
+begin
+
+lemma mult_sdiv_smod_eq:
+  \<open>b * (a sdiv b) + a smod b = a\<close>
+  using sdiv_mult_smod_eq [of a b] by (simp add: ac_simps)
+
+lemma smod_sdiv_mult_eq:
+  \<open>a smod b + a sdiv b * b = a\<close>
+  using sdiv_mult_smod_eq [of a b] by (simp add: ac_simps)
+
+lemma smod_mult_sdiv_eq:
+  \<open>a smod b + b * (a sdiv b) = a\<close>
+  using sdiv_mult_smod_eq [of a b] by (simp add: ac_simps)
+
+lemma minus_sdiv_mult_eq_smod:
+  \<open>a - a sdiv b * b = a smod b\<close>
+  by (rule add_implies_diff [symmetric]) (fact smod_sdiv_mult_eq)
+
+lemma minus_mult_sdiv_eq_smod:
+  \<open>a - b * (a sdiv b) = a smod b\<close>
+  by (rule add_implies_diff [symmetric]) (fact smod_mult_sdiv_eq)
+
+lemma minus_smod_eq_sdiv_mult:
+  \<open>a - a smod b = a sdiv b * b\<close>
+  by (rule add_implies_diff [symmetric]) (fact sdiv_mult_smod_eq)
+
+lemma minus_smod_eq_mult_sdiv:
+  \<open>a - a smod b = b * (a sdiv b)\<close>
+  by (rule add_implies_diff [symmetric]) (fact mult_sdiv_smod_eq)
+
+end
 
 instantiation int :: signed_division
 begin
@@ -18,12 +50,45 @@
   where \<open>k sdiv l = sgn k * sgn l * (\<bar>k\<bar> div \<bar>l\<bar>)\<close> for k l :: int
 
 definition signed_modulo_int :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close>
-  where \<open>k smod l = k - (k sdiv l) * l\<close> for k l :: int
+  where \<open>k smod l = sgn k * (\<bar>k\<bar> mod \<bar>l\<bar>)\<close> for k l :: int
 
-instance ..
+instance by standard
+  (simp add: signed_divide_int_def signed_modulo_int_def div_abs_eq mod_abs_eq algebra_simps)
 
 end
 
+lemma divide_int_eq_signed_divide_int:
+  \<open>k div l = k sdiv l - of_bool (l \<noteq> 0 \<and> sgn k \<noteq> sgn l \<and> \<not> l dvd k)\<close>
+  for k l :: int
+  by (simp add: div_eq_div_abs [of k l] signed_divide_int_def)
+
+lemma signed_divide_int_eq_divide_int:
+  \<open>k sdiv l = k div l + of_bool (l \<noteq> 0 \<and> sgn k \<noteq> sgn l \<and> \<not> l dvd k)\<close>
+  for k l :: int
+  by (simp add: divide_int_eq_signed_divide_int)
+
+lemma modulo_int_eq_signed_modulo_int:
+  \<open>k mod l = k smod l + l * of_bool (sgn k \<noteq> sgn l \<and> \<not> l dvd k)\<close>
+  for k l :: int
+  by (simp add: mod_eq_mod_abs [of k l] signed_modulo_int_def)
+
+lemma signed_modulo_int_eq_modulo_int:
+  \<open>k smod l = k mod l - l * of_bool (sgn k \<noteq> sgn l \<and> \<not> l dvd k)\<close>
+  for k l :: int
+  by (simp add: modulo_int_eq_signed_modulo_int)
+
+lemma sdiv_int_div_0:
+  "(x :: int) sdiv 0 = 0"
+  by (clarsimp simp: signed_divide_int_def)
+
+lemma sdiv_int_0_div [simp]:
+  "0 sdiv (x :: int) = 0"
+  by (clarsimp simp: signed_divide_int_def)
+
+lemma smod_int_alt_def:
+     "(a::int) smod b = sgn (a) * (abs a mod abs b)"
+  by (fact signed_modulo_int_def)
+
 lemma int_sdiv_simps [simp]:
     "(a :: int) sdiv 1 = a"
     "(a :: int) sdiv 0 = 0"
@@ -31,11 +96,13 @@
   apply (auto simp: signed_divide_int_def sgn_if)
   done
 
-lemma sgn_div_eq_sgn_mult:
-    "a div b \<noteq> 0 \<Longrightarrow> sgn ((a :: int) div b) = sgn (a * b)"
-  apply (clarsimp simp: sgn_if zero_le_mult_iff neg_imp_zdiv_nonneg_iff not_less)
-  apply (metis less_le mult_le_0_iff neg_imp_zdiv_neg_iff not_less pos_imp_zdiv_neg_iff zdiv_eq_0_iff)
-  done
+lemma smod_int_mod_0 [simp]:
+  "x smod (0 :: int) = x"
+  by (clarsimp simp: signed_modulo_int_def abs_mult_sgn ac_simps)
+
+lemma smod_int_0_mod [simp]:
+  "0 smod (x :: int) = 0"
+  by (clarsimp simp: smod_int_alt_def)
 
 lemma sgn_sdiv_eq_sgn_mult:
   "a sdiv b \<noteq> 0 \<Longrightarrow> sgn ((a :: int) sdiv b) = sgn (a * b)"
@@ -71,38 +138,17 @@
   done
 
 lemma sdiv_int_range:
-    "(a :: int) sdiv b \<in> { - (abs a) .. (abs a) }"
-  apply (unfold signed_divide_int_def)
-  apply (subgoal_tac "(abs a) div (abs b) \<le> (abs a)")
-   apply (auto simp add: sgn_if not_less)
-      apply (metis le_less le_less_trans neg_equal_0_iff_equal neg_less_iff_less not_le pos_imp_zdiv_neg_iff)
-     apply (metis add.inverse_neutral div_int_pos_iff le_less neg_le_iff_le order_trans)
-    apply (metis div_minus_right le_less_trans neg_imp_zdiv_neg_iff neg_less_0_iff_less not_le)
-  using div_int_pos_iff apply fastforce
-  apply (auto simp add: abs_if not_less)
-     apply (metis add.inverse_inverse add_0_left div_by_1 div_minus_right less_le neg_0_le_iff_le not_le not_one_le_zero zdiv_mono2 zless_imp_add1_zle)
-    apply (metis div_by_1 neg_0_less_iff_less pos_imp_zdiv_pos_iff zdiv_mono2 zero_less_one)
-   apply (metis add.inverse_neutral div_by_0 div_by_1 int_div_less_self int_one_le_iff_zero_less less_le less_minus_iff order_refl)
-  apply (metis div_by_1 divide_int_def int_div_less_self less_le linorder_neqE_linordered_idom order_refl unique_euclidean_semiring_numeral_class.div_less)
-  done
-
-lemma sdiv_int_div_0 [simp]:
-  "(x :: int) sdiv 0 = 0"
-  by (clarsimp simp: signed_divide_int_def)
-
-lemma sdiv_int_0_div [simp]:
-  "0 sdiv (x :: int) = 0"
-  by (clarsimp simp: signed_divide_int_def)
-
-lemma smod_int_alt_def:
-     "(a::int) smod b = sgn (a) * (abs a mod abs b)"
-  apply (clarsimp simp: signed_modulo_int_def signed_divide_int_def)
-  apply (clarsimp simp: minus_div_mult_eq_mod [symmetric] abs_sgn sgn_mult sgn_if algebra_split_simps)
-  done
+  \<open>a sdiv b \<in> {- \<bar>a\<bar>..\<bar>a\<bar>}\<close> for a b :: int
+  using zdiv_mono2 [of \<open>\<bar>a\<bar>\<close> 1 \<open>\<bar>b\<bar>\<close>]
+  by (cases \<open>b = 0\<close>; cases \<open>sgn b = sgn a\<close>)
+     (auto simp add: signed_divide_int_def pos_imp_zdiv_nonneg_iff
+     dest!: sgn_not_eq_imp intro: order_trans [of _ 0])
 
 lemma smod_int_range:
-  "b \<noteq> 0 \<Longrightarrow> (a::int) smod b \<in> { - abs b + 1 .. abs b - 1 }"
-  apply (case_tac  "b > 0")
+  \<open>a smod b \<in> {- \<bar>b\<bar> + 1..\<bar>b\<bar> - 1}\<close>
+  if \<open>b \<noteq> 0\<close> for a b :: int
+  using that
+  apply (cases \<open>b > 0\<close>)
    apply (insert pos_mod_conj [where a=a and b=b])[1]
    apply (insert pos_mod_conj [where a="-a" and b=b])[1]
    apply (auto simp: smod_int_alt_def algebra_simps sgn_if
@@ -129,14 +175,6 @@
   apply (auto simp: add1_zle_eq smod_int_alt_def sgn_if)
   done
 
-lemma smod_int_mod_0 [simp]:
-  "x smod (0 :: int) = x"
-  by (clarsimp simp: signed_modulo_int_def)
-
-lemma smod_int_0_mod [simp]:
-  "0 smod (x :: int) = 0"
-  by (clarsimp simp: smod_int_alt_def)
-
 lemma smod_mod_positive:
     "\<lbrakk> 0 \<le> (a :: int); 0 \<le> b \<rbrakk> \<Longrightarrow> a smod b = a mod b"
   by (clarsimp simp: smod_int_alt_def zsgn_def)

--- a/src/HOL/Numeral_Simprocs.thy	Sat Aug 20 21:33:51 2022 +0200
+++ b/src/HOL/Numeral_Simprocs.thy	Sat Aug 20 21:34:55 2022 +0200
@@ -15,14 +15,11 @@
 lemmas semiring_norm =
   Let_def arith_simps diff_nat_numeral rel_simps
   if_False if_True
-  add_0 add_Suc add_numeral_left
+  add_Suc add_numeral_left
   add_neg_numeral_left mult_numeral_left
   numeral_One [symmetric] uminus_numeral_One [symmetric] Suc_eq_plus1
   eq_numeral_iff_iszero not_iszero_Numeral1
 
-declare split_div [of _ _ "numeral k", arith_split] for k
-declare split_mod [of _ _ "numeral k", arith_split] for k
-
 text \<open>For \<open>combine_numerals\<close>\<close>
 
 lemma left_add_mult_distrib: "i*u + (j*u + k) = (i+j)*u + (k::nat)"
@@ -92,16 +89,16 @@
 lemma nat_mult_eq_cancel_disj:
   fixes k m n :: nat
   shows "k * m = k * n \<longleftrightarrow> k = 0 \<or> m = n"
-  by auto
+  by (fact mult_cancel_left)
 
-lemma nat_mult_div_cancel_disj [simp]:
+lemma nat_mult_div_cancel_disj:
   fixes k m n :: nat
   shows "(k * m) div (k * n) = (if k = 0 then 0 else m div n)"
   by (fact div_mult_mult1_if)
 
 lemma numeral_times_minus_swap:
   fixes x:: "'a::comm_ring_1" shows  "numeral w * -x = x * - numeral w"
-  by (simp add: mult.commute)
+  by (simp add: ac_simps)
 
 ML_file \<open>Tools/numeral_simprocs.ML\<close>
 

--- a/src/HOL/Rings.thy	Sat Aug 20 21:33:51 2022 +0200
+++ b/src/HOL/Rings.thy	Sat Aug 20 21:34:55 2022 +0200
@@ -560,6 +560,26 @@
   then show "a * a = b * b" by auto
 qed
 
+lemma inj_mult_left [simp]: \<open>inj ((*) a) \<longleftrightarrow> a \<noteq> 0\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
+proof
+  assume ?P
+  show ?Q
+  proof
+    assume \<open>a = 0\<close>
+    with \<open>?P\<close> have "inj ((*) 0)"
+      by simp
+    moreover have "0 * 0 = 0 * 1"
+      by simp
+    ultimately have "0 = 1"
+      by (rule injD)
+    then show False
+      by simp
+  qed
+next
+  assume ?Q then show ?P
+    by (auto intro: injI)
+qed
+
 end
 
 class idom_abs_sgn = idom + abs + sgn +
@@ -2567,6 +2587,10 @@
   "sgn a * sgn a = of_bool (a \<noteq> 0)"
   by (cases "a > 0") simp_all
 
+lemma left_sgn_mult_self_eq [simp]:
+  \<open>sgn a * (sgn a * b) = of_bool (a \<noteq> 0) * b\<close>
+  by (simp flip: mult.assoc)
+
 lemma abs_mult_self_eq [simp]:
   "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
   by (cases "a > 0") simp_all
@@ -2647,6 +2671,12 @@
   shows "x+y < 0 \<Longrightarrow> x<0 \<or> y<0"
   by (auto simp: not_less intro: le_less_trans [of _ "x+y"])
 
+text \<open>
+  Is this really better than just rewriting with \<open>abs_if\<close>?
+\<close>
+lemma abs_split [no_atp]: \<open>P \<bar>a\<bar> \<longleftrightarrow> (0 \<le> a \<longrightarrow> P a) \<and> (a < 0 \<longrightarrow> P (- a))\<close>
+  by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
+
 end
 
 text \<open>Reasoning about inequalities with division\<close>

--- a/src/HOL/Tools/SMT/smt_systems.ML	Sat Aug 20 21:33:51 2022 +0200
+++ b/src/HOL/Tools/SMT/smt_systems.ML	Sat Aug 20 21:34:55 2022 +0200
@@ -104,13 +104,13 @@
   smt_options = [(":produce-unsat-cores", "true")],
   good_slices =
     (* FUDGE *)
-    [((1, 512, meshN), ["--full-saturate-quant", "--inst-when=full-last-call", "--inst-no-entail", "--term-db-mode=relevant", "--multi-trigger-linear"]),
-     ((1, 64, meshN), ["--decision=internal", "--simplification=none", "--full-saturate-quant"]),
-     ((1, 1024, meshN), ["--relevant-triggers", "--full-saturate-quant"]),
-     ((1, 256, mepoN), ["--trigger-sel=max", "--full-saturate-quant"]),
-     ((1, 32, meshN), ["--term-db-mode=relevant", "--full-saturate-quant"]),
-     ((1, 128, meshN), ["--no-e-matching", "--full-saturate-quant"]),
-     ((1, 256, meshN), ["--finite-model-find", "--fmf-inst-engine"])],
+    [((2, 512, meshN), ["--full-saturate-quant", "--inst-when=full-last-call", "--inst-no-entail", "--term-db-mode=relevant", "--multi-trigger-linear"]),
+     ((2, 64, meshN), ["--decision=internal", "--simplification=none", "--full-saturate-quant"]),
+     ((2, 1024, meshN), ["--relevant-triggers", "--full-saturate-quant"]),
+     ((2, 256, mepoN), ["--trigger-sel=max", "--full-saturate-quant"]),
+     ((2, 32, meshN), ["--term-db-mode=relevant", "--full-saturate-quant"]),
+     ((2, 128, meshN), ["--no-e-matching", "--full-saturate-quant"]),
+     ((2, 256, meshN), ["--finite-model-find", "--fmf-inst-engine"])],
   outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"),
   parse_proof = SOME (K CVC_Proof_Parse.parse_proof),
   replay = NONE }
@@ -124,13 +124,13 @@
   smt_options = [(":produce-unsat-cores", "true")],
   good_slices =
     (* FUDGE *)
-    [((1, 512, meshN), ["--full-saturate-quant", "--inst-when=full-last-call", "--inst-no-entail", "--term-db-mode=relevant", "--multi-trigger-linear"]),
-     ((1, 64, meshN), ["--decision=internal", "--simplification=none", "--full-saturate-quant"]),
-     ((1, 1024, meshN), ["--relevant-triggers", "--full-saturate-quant"]),
-     ((1, 256, mepoN), ["--trigger-sel=max", "--full-saturate-quant"]),
-     ((1, 32, meshN), ["--term-db-mode=relevant", "--full-saturate-quant"]),
-     ((1, 128, meshN), ["--no-e-matching", "--full-saturate-quant"]),
-     ((1, 256, meshN), ["--finite-model-find", "--fmf-inst-engine"])],
+    [((2, 512, meshN), ["--full-saturate-quant", "--inst-when=full-last-call", "--inst-no-entail", "--term-db-mode=relevant", "--multi-trigger-linear"]),
+     ((2, 64, meshN), ["--decision=internal", "--simplification=none", "--full-saturate-quant"]),
+     ((2, 1024, meshN), ["--relevant-triggers", "--full-saturate-quant"]),
+     ((2, 256, mepoN), ["--trigger-sel=max", "--full-saturate-quant"]),
+     ((2, 32, meshN), ["--term-db-mode=relevant", "--full-saturate-quant"]),
+     ((2, 128, meshN), ["--no-e-matching", "--full-saturate-quant"]),
+     ((2, 256, meshN), ["--finite-model-find", "--fmf-inst-engine"])],
   outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"),
   parse_proof = SOME (K CVC_Proof_Parse.parse_proof),
   replay = NONE }
@@ -169,12 +169,12 @@
   smt_options = [(":produce-proofs", "true")],
   good_slices =
     (* FUDGE *)
-    [((1, 1024, meshN), []),
-     ((1, 512, mashN), []),
-     ((1, 64, meshN), []),
-     ((1, 128, meshN), []),
-     ((1, 256, mepoN), []),
-     ((1, 32, meshN), [])],
+    [((2, 1024, meshN), []),
+     ((2, 512, mashN), []),
+     ((2, 64, meshN), []),
+     ((2, 128, meshN), []),
+     ((2, 256, mepoN), []),
+     ((2, 32, meshN), [])],
   outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" "unknown" "Time limit exceeded"),
   parse_proof = SOME (K Lethe_Proof_Parse.parse_proof),
   replay = SOME Verit_Replay.replay }
@@ -210,12 +210,12 @@
   smt_options = [(":produce-proofs", "true")],
   good_slices =
     (* FUDGE *)
-    [((1, 1024, meshN), []),
-     ((1, 512, mepoN), []),
-     ((1, 64, meshN), []),
-     ((1, 256, meshN), []),
-     ((1, 128, mashN), []),
-     ((1, 32, meshN), [])],
+    [((2, 1024, meshN), []),
+     ((2, 512, mepoN), []),
+     ((2, 64, meshN), []),
+     ((2, 256, meshN), []),
+     ((2, 128, mashN), []),
+     ((2, 32, meshN), [])],
   outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"),
   parse_proof = SOME Z3_Replay.parse_proof,
   replay = SOME Z3_Replay.replay }

--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sat Aug 20 21:33:51 2022 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sat Aug 20 21:34:55 2022 +0200
@@ -300,10 +300,13 @@
     cat_lines (map (fn (filter, facts) => string_of_facts filter facts) factss)
 
 val default_slice_schedule =
-  (* FUDGE (inspired by Seventeen evaluation) *)
-  [cvc4N, zipperpositionN, vampireN, veritN, eN, cvc4N, zipperpositionN, cvc4N, vampireN, cvc4N,
-   cvc4N, vampireN, cvc4N, iproverN, zipperpositionN, vampireN, vampireN, zipperpositionN, z3N,
-   zipperpositionN, vampireN, iproverN, vampireN, cvc4N, z3N, z3N, cvc4N, cvc4N]
+  (* FUDGE (loosely inspired by Seventeen evaluation) *)
+  [cvc4N, zipperpositionN, vampireN, veritN, spassN, zipperpositionN, eN, cvc4N,
+   zipperpositionN, cvc4N, zipperpositionN, vampireN, cvc4N, cvc4N, vampireN,
+   cvc4N, iproverN, zipperpositionN, spassN, vampireN, zipperpositionN,
+   vampireN, zipperpositionN, z3N, zipperpositionN, vampireN, iproverN, spassN,
+   zipperpositionN, vampireN, cvc4N, zipperpositionN, z3N, z3N, cvc4N, cvc4N,
+   zipperpositionN]
 
 fun schedule_of_provers provers num_slices =
   let

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Sat Aug 20 21:33:51 2022 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Sat Aug 20 21:34:55 2022 +0200
@@ -139,7 +139,7 @@
    prem_role = Hypothesis,
    good_slices =
      (* FUDGE *)
-     K [((1, 60, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))],
+     K [((2, 60, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))],
    good_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
    good_max_new_mono_instances = default_max_new_mono_instances}
 
@@ -223,11 +223,11 @@
    prem_role = Hypothesis,
    good_slices =
      (* FUDGE *)
-     K [((1, 32, meshN), (TF0, "mono_native", liftingN, false, "")),
-       ((1, 512, meshN), (TX0, "mono_native", liftingN, false, "")),
-       ((1, 128, mashN), (TF0, "mono_native", combsN, false, "")),
-       ((1, 1024, meshN), (TF0, "mono_native", liftingN, false, "")),
-       ((1, 256, mepoN), (TF0, "mono_native", combsN, false, ""))],
+     K [((2, 32, meshN), (TF0, "mono_native", liftingN, false, "")),
+       ((2, 512, meshN), (TX0, "mono_native", liftingN, false, "")),
+       ((2, 128, mashN), (TF0, "mono_native", combsN, false, "")),
+       ((2, 1024, meshN), (TF0, "mono_native", liftingN, false, "")),
+       ((2, 256, mepoN), (TF0, "mono_native", combsN, false, ""))],
    good_max_mono_iters = default_max_mono_iters,
    good_max_new_mono_instances = default_max_new_mono_instances}
 
@@ -252,7 +252,7 @@
    prem_role = Hypothesis,
    good_slices =
      (* FUDGE *)
-     K [((1, 40, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))],
+     K [((2, 40, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))],
    good_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
    good_max_new_mono_instances = default_max_new_mono_instances}
 
@@ -273,8 +273,8 @@
    prem_role = Hypothesis,
    good_slices =
      (* FUDGE *)
-     K [((3, 512, meshN), (TH0, "mono_native_higher", keep_lamsN, false, "")),
-       ((3, 512, meshN), (TF0, "mono_native", liftingN, false, ""))],
+     K [((6, 512, meshN), (TH0, "mono_native_higher", keep_lamsN, false, "")),
+       ((6, 512, meshN), (TF0, "mono_native", liftingN, false, ""))],
    good_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
    good_max_new_mono_instances = default_max_new_mono_instances}
 
@@ -297,7 +297,7 @@
    prem_role = Hypothesis,
    good_slices =
      (* FUDGE *)
-     K [((6, 256, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))],
+     K [((12, 256, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))],
    good_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
    good_max_new_mono_instances = default_max_new_mono_instances}
 
@@ -334,14 +334,14 @@
      prem_role = Conjecture,
      good_slices =
        (* FUDGE *)
-       K [((1, 150, meshN), (format, "mono_native", combsN, true, "")),
-        ((1, 500, meshN), (format, "mono_native", liftingN, true, spass_H2SOS)),
-        ((1, 50, meshN), (format,  "mono_native", liftingN, true, spass_H2LR0LT0)),
-        ((1, 250, meshN), (format, "mono_native", combsN, true, spass_H2NuVS0)),
-        ((1, 1000, mepoN), (format, "mono_native", liftingN, true, spass_H1SOS)),
-        ((1, 150, meshN), (format, "poly_guards??", liftingN, false, spass_H2NuVS0Red2)),
-        ((1, 300, meshN), (format, "mono_native", combsN, true, spass_H2SOS)),
-        ((1, 100, meshN), (format, "mono_native", combs_and_liftingN, true, spass_H2))],
+       K [((2, 150, meshN), (format, "mono_native", combsN, true, "")),
+        ((2, 500, meshN), (format, "mono_native", liftingN, true, spass_H2SOS)),
+        ((2, 50, meshN), (format,  "mono_native", liftingN, true, spass_H2LR0LT0)),
+        ((2, 250, meshN), (format, "mono_native", combsN, true, spass_H2NuVS0)),
+        ((2, 1000, mepoN), (format, "mono_native", liftingN, true, spass_H1SOS)),
+        ((2, 150, meshN), (format, "poly_guards??", liftingN, false, spass_H2NuVS0Red2)),
+        ((2, 300, meshN), (format, "mono_native", combsN, true, spass_H2SOS)),
+        ((2, 100, meshN), (format, "mono_native", combs_and_liftingN, true, spass_H2))],
      good_max_mono_iters = default_max_mono_iters,
      good_max_new_mono_instances = default_max_new_mono_instances}
   end
@@ -380,14 +380,14 @@
    prem_role = Hypothesis,
    good_slices =
      (* FUDGE *)
-     K [((1, 512, meshN), (TX1, "mono_native_fool", combsN, false, sosN)),
-      ((1, 1024, meshN), (TX1, "mono_native_fool", liftingN, false, sosN)),
-      ((1, 256, mashN), (TX1, "mono_native_fool", liftingN, false, no_sosN)),
-      ((1, 512, mepoN), (TF1, "poly_native", liftingN, false, no_sosN)),
-      ((1, 16, meshN), (TX1, "mono_native_fool", liftingN, false, no_sosN)),
-      ((1, 32, meshN), (TX1, "mono_native_fool", combsN, false, no_sosN)),
-      ((1, 64, meshN), (TX1, "mono_native_fool", combs_or_liftingN, false, no_sosN)),
-      ((1, 128, meshN), (TX1, "mono_native_fool", liftingN, false, no_sosN))],
+     K [((2, 512, meshN), (TX1, "mono_native_fool", combsN, false, sosN)),
+      ((2, 1024, meshN), (TX1, "mono_native_fool", liftingN, false, sosN)),
+      ((2, 256, mashN), (TX1, "mono_native_fool", liftingN, false, no_sosN)),
+      ((2, 512, mepoN), (TF1, "poly_native", liftingN, false, no_sosN)),
+      ((2, 16, meshN), (TX1, "mono_native_fool", liftingN, false, no_sosN)),
+      ((2, 32, meshN), (TX1, "mono_native_fool", combsN, false, no_sosN)),
+      ((2, 64, meshN), (TX1, "mono_native_fool", combs_or_liftingN, false, no_sosN)),
+      ((2, 128, meshN), (TX1, "mono_native_fool", liftingN, false, no_sosN))],
    good_max_mono_iters = default_max_mono_iters,
    good_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)}
 
@@ -411,12 +411,21 @@
        known_szs_status_failures,
      prem_role = Hypothesis,
      good_slices =
-       K [((1, 256, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --boolean-reasoning=simpl-only --ho-unif-max-depth=0 --ho-prim-enum=none -q \"2|prefer-ho-steps|conjecture-relative-e(0.1,0.5,100,100,100,100,1.5,1.5,1.5)\" -q \"1|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"2|prefer-ground|default\" -q \"2|prefer-empty-trail|conjecture-relative-e(0.1,0.5,100,100,100,100,1.5,1.5,1.5)\" -q \"1|prefer-processed|fifo\" --select=bb+e-selection7 --ho-pattern-decider=false --ho-fixpoint-decider=true --ho-solid-decider=false --sine=150 --sine-tolerance=2 --sine-depth-max=3 --sine-depth-min=1 --prec-gen-fun=invfreqhack --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=2 --fluid-log-hoist=false --tptp-def-as-rewrite --rewrite-before-cnf=true --ho-prim-enum=eq --ho-prim-enum-add-var=true --ho-prim-max=1 --ho-prim-enum-early-bird=true -o tptp --avatar=eager --split-only-ground=true")),
-         ((1, 64, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-comb-complete --boolean-reasoning=simpl-only --ext-rules=off --kbo-weight-fun=lambda-def-sqarity --ho-prim-enum=none --tptp-def-as-rewrite -q \"4|prefer-sos|orient-lmax(2,1,2,1,1)\" -q \"4|defer-sos|conjecture-relative-var(1,s,f)\" -q \"3|const|default\" -q \"1|prefer-processed|fifo\" --ho-elim-leibniz=1 --select=NoSelection --solve-formulas=true --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=8 --sine=60 --sine-tolerance=2 --sine-depth-max=5 --sine-depth-min=1 --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=3 --e-auto=true --e-max-derived=50 --e-encode-lambdas=ignore --scan-clause-ac=false --presaturate=true --comb-b-penalty=3 --comb-c-penalty=3 --comb-k-penalty=1 --comb-s-penalty=5 --subvarsup=false --e-call-point=0.15 --lazy-cnf-kind=simp --trigger-bool-ind=1")),
-         ((1, 32, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic -nc --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=ext-family --ext-rules-max-depth=1 --ho-prim-enum=none --avatar=off --recognize-injectivity=true --ho-elim-leibniz=1 --ho-unif-level=pragmatic-framework --no-max-vars --max-inferences=4 --ho-max-app-projections=1 --ho-max-elims=0 --ho-max-rigid-imitations=2 --ho-max-identifications=0 --ho-unif-max-depth=3 -q \"6|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"6|const|conjecture-relative-var(1.02,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-easy-ho|conjecture-relative-var(1.01,s,f)\" --select=e-selection7 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=7 --sine=50 --sine-tolerance=1 --sine-depth-max=2 --sine-depth-min=1 --e-max-derived=64 --sine-ignore-k-most-common-syms=2 --sine-trim-implications=true --e-encode-lambdas=lift --scan-clause-ac=false --lambdasup=0 --kbo-weight-fun=lambda-def-invfreqrank --demod-in-var-args=true --bool-demod=true --lambda-demod=true --e-call-point=0.1 --lazy-cnf-kind=simp")),
-         ((1, 512, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=ext-family --ext-rules-max-depth=1 --ho-prim-enum=none --avatar=off --recognize-injectivity=true --ho-elim-leibniz=1 --ho-unif-level=pragmatic-framework --no-max-vars --max-inferences=2 --ho-unif-max-depth=1 -q \"6|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"6|const|conjecture-relative-var(1.02,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-easy-ho|conjecture-relative-var(1.01,s,f)\" --select=e-selection16 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=3 --e-auto=true --sine=50 --sine-tolerance=1.0 --sine-depth-max=3 --sine-depth-min=1 --sine-trim-implications=true --ho-unif-level=pragmatic-framework --e-encode-lambdas=lift --scan-clause-ac=false --kbo-weight-fun=lambda-def-invfreqrank --e-call-point=0.1")),         
-         ((1, 1024, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --max-inferences=1 --ho-unif-max-depth=1 --ho-max-elims=0 --ho-max-app-projections=0 --ho-max-rigid-imitations=1 --ho-max-identifications=0 --boolean-reasoning=bool-hoist --bool-hoist-simpl=true --bool-select=LI --recognize-injectivity=true --ext-rules=ext-family --ext-rules-max-depth=1 --ho-choice-inst=true --ho-prim-enum=none --ho-elim-leibniz=0 --interpret-bool-funs=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --ho-unif-level=pragmatic-framework --select=bb+e-selection2 --post-cnf-lambda-lifting=true -q \"4|prefer-sos|pnrefined(2,1,1,1,2,2,2)\" -q \"6|prefer-processed|conjecture-relative-struct(1.5,3.5,2,3)\" -q \"1|const|fifo\" -q \"4|prefer-ground|orient-lmax(2,1,2,1,1)\" -q \"4|defer-sos|conjecture-relative-struct(1,5,2,3)\" --avatar=off --recognize-injectivity=true --ho-neg-ext=true --e-timeout=2 --ho-pattern-decider=true --ho-fixpoint-decider=true --e-max-derived=50 --ignore-orphans=true --e-auto=true --presaturate=true --e-call-point=0.1")),
-         ((1, 128, mepoN), (format, "mono_native_higher_fool", keep_lamsN, false, "-nc --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=off --ho-prim-enum=full --ho-prim-max=1 --avatar=off --recognize-injectivity=true --ho-elim-leibniz=4 --ho-unif-level=full-framework --no-max-vars -q \"2|prefer-goals|conjecture-relative-e(0.5,1,100,100,100,100,1.5,1.5,1)\" -q \"4|const|conjecture-relative-e(0.1,1,100,100,100,100,1.5,1.5,1.5)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-e(0.5,1,100,100,100,100,1.5,1.5,1.5)\" -q \"4|prefer-sos|pnrefined(1,1,1,1,2,1.5,2)\" --select=ho-selection5 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=5 --e-call-point=0.25 --e-auto=true --sine=50 --sine-tolerance=2 --sine-depth-max=4 --sine-depth-min=1 --e-max-derived=96 --e-encode-lambdas=lift --scan-clause-ac=false --kbo-weight-fun=arity0 --prec-gen-fun=invfreq_conj"))],
+       K [((1, 512, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --max-inferences=1 --ho-unif-max-depth=1 --ho-max-elims=0 --ho-max-app-projections=0 --ho-max-rigid-imitations=1 --ho-max-identifications=0 --boolean-reasoning=bool-hoist --bool-hoist-simpl=true --bool-select=LI --recognize-injectivity=true --ext-rules=ext-family --ext-rules-max-depth=1 --ho-choice-inst=true --ho-prim-enum=none --ho-elim-leibniz=0 --interpret-bool-funs=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --ho-unif-level=pragmatic-framework --select=bb+e-selection2 --post-cnf-lambda-lifting=true -q \"4|prefer-sos|pnrefined(2,1,1,1,2,2,2)\" -q \"6|prefer-processed|conjecture-relative-struct(1.5,3.5,2,3)\" -q \"1|const|fifo\" -q \"4|prefer-ground|orient-lmax(2,1,2,1,1)\" -q \"4|defer-sos|conjecture-relative-struct(1,5,2,3)\" --avatar=off --recognize-injectivity=true --ho-neg-ext=true --e-timeout=2 --ho-pattern-decider=true --ho-fixpoint-decider=true --e-max-derived=50 --ignore-orphans=true --e-auto=true --presaturate=true --e-call-point=0.1")),  (* sh5_sh1.sh *)
+          ((1, 1024, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=ext-family --ext-rules-max-depth=1 --ho-prim-enum=none --avatar=off --recognize-injectivity=true --ho-elim-leibniz=1 --ho-unif-level=pragmatic-framework --no-max-vars --max-inferences=2 --ho-unif-max-depth=1 -q \"6|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"6|const|conjecture-relative-var(1.02,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-easy-ho|conjecture-relative-var(1.01,s,f)\" --select=e-selection16 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=3 --e-auto=true --sine=50 --sine-tolerance=1.0 --sine-depth-max=3 --sine-depth-min=1 --sine-trim-implications=true --ho-unif-level=pragmatic-framework --e-encode-lambdas=lift --scan-clause-ac=false --kbo-weight-fun=lambda-def-invfreqrank --e-call-point=0.1")),  (* sh8_shallow_sine.sh *)
+          ((1, 256, mepoN), (format, "mono_native_higher_fool", keep_lamsN, false, "-nc --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=off --ho-prim-enum=full --ho-prim-max=1 --avatar=off --recognize-injectivity=true --ho-elim-leibniz=4 --ho-unif-level=full-framework --no-max-vars -q \"2|prefer-goals|conjecture-relative-e(0.5,1,100,100,100,100,1.5,1.5,1)\" -q \"4|const|conjecture-relative-e(0.1,1,100,100,100,100,1.5,1.5,1.5)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-e(0.5,1,100,100,100,100,1.5,1.5,1.5)\" -q \"4|prefer-sos|pnrefined(1,1,1,1,2,1.5,2)\" --select=ho-selection5 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=5 --e-call-point=0.25 --e-auto=true --sine=50 --sine-tolerance=2 --sine-depth-max=4 --sine-depth-min=1 --e-max-derived=96 --e-encode-lambdas=lift --scan-clause-ac=false --kbo-weight-fun=arity0 --prec-gen-fun=invfreq_conj")),  (* sh10_new_c.s3.sh *)
+          ((1, 512, mepoN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic -nc --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=ext-family --ext-rules-max-depth=1 --ho-prim-enum=none --avatar=off --recognize-injectivity=true --ho-elim-leibniz=1 --ho-unif-level=pragmatic-framework --no-max-vars --max-inferences=4 --ho-max-app-projections=1 --ho-max-elims=0 --ho-max-rigid-imitations=2 --ho-max-identifications=0 --ho-unif-max-depth=3 -q \"6|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"6|const|conjecture-relative-var(1.02,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-easy-ho|conjecture-relative-var(1.01,s,f)\" --select=e-selection7 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=7 --sine=50 --sine-tolerance=1 --sine-depth-max=2 --sine-depth-min=1 --e-max-derived=64 --sine-ignore-k-most-common-syms=2 --sine-trim-implications=true --e-encode-lambdas=lift --scan-clause-ac=false --lambdasup=0 --kbo-weight-fun=lambda-def-invfreqrank --demod-in-var-args=true --bool-demod=true --lambda-demod=true --e-call-point=0.1")),  (* sh10_c_ic.sh *)
+          ((1, 512, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-comb-complete --boolean-reasoning=simpl-only --ext-rules=off --kbo-weight-fun=lambda-def-sqarity --ho-prim-enum=none --tptp-def-as-rewrite -q \"4|prefer-sos|orient-lmax(2,1,2,1,1)\" -q \"4|defer-sos|conjecture-relative-var(1,s,f)\" -q \"3|const|default\" -q \"1|prefer-processed|fifo\" --ho-elim-leibniz=1 --select=NoSelection --solve-formulas=true --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=8 --sine=60 --sine-tolerance=2 --sine-depth-max=5 --sine-depth-min=1 --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=3 --e-auto=true --e-max-derived=50 --e-encode-lambdas=lift --scan-clause-ac=false --presaturate=true --comb-b-penalty=3 --comb-c-penalty=3 --comb-k-penalty=1 --comb-s-penalty=5 --subvarsup=false --e-call-point=0.15")),  (* sh8_b.comb.sh (modified) *)
+          ((1, 1024, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --boolean-reasoning=simpl-only --ho-unif-max-depth=0 --ho-prim-enum=none -q \"2|prefer-ho-steps|conjecture-relative-e(0.1,0.5,100,100,100,100,1.5,1.5,1.5)\" -q \"1|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"2|prefer-ground|default\" -q \"2|prefer-empty-trail|conjecture-relative-e(0.1,0.5,100,100,100,100,1.5,1.5,1.5)\" -q \"1|prefer-processed|fifo\" --select=bb+e-selection7 --ho-pattern-decider=false --ho-fixpoint-decider=true --ho-solid-decider=false --sine=150 --sine-tolerance=2 --sine-depth-max=3 --sine-depth-min=1 --prec-gen-fun=invfreqhack --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=2 --fluid-log-hoist=false --tptp-def-as-rewrite --rewrite-before-cnf=true --ho-prim-enum=eq --ho-prim-enum-add-var=true --ho-prim-max=1 --ho-prim-enum-early-bird=true --avatar=eager --split-only-ground=true")),  (* sh5_add_var_l_av.sh *)
+          ((1, 256, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --max-inferences=4 --ho-max-app-projections=1 --ho-max-elims=0 --ho-max-rigid-imitations=2 --ho-max-identifications=0 --ho-unif-max-depth=2 --max-inferences=3 --boolean-reasoning=bool-hoist --bool-select=LO --ext-rules=off --kbo-weight-fun=lambda-def-invfreqrank --ho-prim-enum=none --ho-unif-level=pragmatic-framework -q \"1|prefer-sos|conjecture-relative-var(1.01,s,f)\" -q \"4|const|conjecture-relative-var(1.05,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1.02,l,f)\" -q \"4|prefer-sos|pnrefined(3,2,3,2,2,1.5,2)\" --ho-elim-leibniz=1 --ho-fixpoint-decider=true --ho-pattern-decider=true --ho-solid-decider=true --select=e-selection2 --solve-formulas=true --lambdasup=0 --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=3 --e-max-derived=48 --e-encode-lambdas=lift --presaturate=true --prec-gen-fun=invfreq --e-call-point=0.2 --e-auto=true --sine-trim-implications=true")),  (* sh10_e_lift.sh *)
+          ((1, 512, mepoN), (format, "mono_native_higher_fool", keep_lamsN, false, "-nc --tptp-def-as-rewrite --mode=ho-pragmatic --max-inferences=4 --ho-max-app-projections=1 --ho-max-elims=0 --ho-max-rigid-imitations=1 --ho-max-identifications=0 --ho-unif-max-depth=2 --boolean-reasoning=simpl-only --ext-rules=off --kbo-weight-fun=lambda-def-const --ho-prim-enum=neg --ho-prim-enum-early-bird=true --tptp-def-as-rewrite --rewrite-before-cnf=true --ho-unif-level=pragmatic-framework --ho-unif-max-depth=1 --sine=50 --sine-tolerance=1.0 --sine-depth-max=3 --sine-depth-min=1 --sine-trim-implications=true -q \"4|prefer-sos|orient-lmax(2,1,2,1,1)\" -q \"4|defer-sos|conjecture-relative-var(1,s,f)\" -q \"3|const|default\" -q \"1|prefer-processed|fifo\" --ho-elim-leibniz=1 --ho-fixpoint-decider=true --ho-pattern-decider=true --ho-solid-decider=false --select=e-selection10 --solve-formulas=true --sup-at-vars=false --sup-at-var-headed=false --sup-from-var-headed=true --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=4 --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=2 --e-auto=true --e-max-derived=32 --e-encode-lambdas=lift --scan-clause-ac=false --presaturate=true --e-call-point=0.16")),  (* sh5_shallow_sine.sh *)
+          ((1, 512, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "-nc --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=bool-hoist --ext-rules=off --recognize-injectivity=true --ho-unif-level=full-framework -q \"4|prefer-goals|pnrefined(1,1,1,2,2,2,0.5)\" -q \"1|prefer-fo|conjecture-relative-var(1.02,l,f)\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-ho-steps|conjecture-relative-var(1.01,s,f)\" -q \"1|prefer-processed|fifo\" --select=bb+ho-selection --scan-clause-ac=false --kbo-weight-fun=invfreqrank --fluidsup=true --boolean-reasoning=bool-hoist --fluid-log-hoist=true --fluid-hoist=true --ite-axioms=true --lazy-cnf=true --ho-solid-decider=true --ho-fixpoint-decider=true --bool-select=\"sel1(pos_ctx)\" --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=2 --e-auto=true --e-call-point=0.35 --avatar=off --e-max-derived=50")),  (* sh5_e_short1.sh *)
+          ((1, 1024, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --boolean-reasoning=simpl-only --select=e-selection12 --prec-gen-fun=invfreq_conj --ord=lambda_kbo --ho-unif-level=full-framework --ho-pattern-decider=true --ho-solid-decider=false --ho-fixpoint-decider=true --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=1 --sine=100 --sine-depth-min=1 --sine-depth-max=5 --sine-tolerance=1.5 -q \"1|prefer-sos|default\" -q \"8|prefer-processed|conjecture-relative-var(1,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-lambdas|explore\" -q \"1|prefer-non-goals|explore\" -q \"1|prefer-processed|conjecture-relative-var(1,s,f)\" --kbo-weight-fun=arity0")),  (* sh5_32.sh *)
+          ((1, 256, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --boolean-reasoning=simpl-only --ho-unif-max-depth=2 --ho-max-app-projections=0 --ho-max-rigid-imitations=1 --ho-max-elims=0 --ho-max-identifications=1 --max-inferences=3 --ext-rules=off --recognize-injectivity=true --ho-prim-enum=none --ho-choice-inst=true -q \"3|prefer-fo|conjecture-relative-var(1.02,l,f)\" -q \"3|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"2|prefer-ground|orient-lmax(2,1,2,1,1)\" -q \"1|prefer-processed|fifo\" --select=MaxGoalNS --sine=60 --sine-tolerance=1.5 --sine-depth-max=3 --sine-depth-min=1 --prec-gen-fun=invfreqhack --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=3 --kbo-weight-fun-from-precedence=true --kbo-weight-fun-from-precedence-rank=5 --trigger-bool-inst=1 --avatar=lazy --tptp-def-as-rewrite --rewrite-before-cnf=true --sup-from-var-headed=false --sup-at-vars=false")),  (* sh5_sh4.sh *)
+          ((1, 512, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "--tptp-def-as-rewrite --rewrite-before-cnf=true --mode=lambda-free-intensional --check-lambda-free=false --boolean-reasoning=simpl-only --post-cnf-lambda-lifting=true --ext-rules=off --ho-prim-enum=none --recognize-injectivity=true --no-max-vars --select=e-selection8 --prec-gen-fun=invfreq --kbo-weight-fun=invfreqrank --kbo-const-weight=2 --ord=lambdafree_kbo --ignore-orphans=true -q \"1|prefer-sos|conjecture-relative-struct(1.5,3.5,2,3)\" -q \"1|const|conj_pref_weight(0.5,100,0.2,0.2,4)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-e(0.3,0.25,100,100,100,100,1.5,1.5,1)\" -q \"1|prefer-sos|pnrefined(3,2,3,2,2,1.5,2)\" --lazy-cnf=true --lazy-cnf-renaming-threshold=2")),  (* sh5_lifting2.sh *)
+          ((1, 512, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "-nc --tptp-def-as-rewrite --rewrite-before-cnf=true --tptp-rewrite-formulas-only=true --mode=ho-pragmatic --boolean-reasoning=simpl-only --ext-rules=ext-family --ext-rules-max-depth=1 --ho-prim-enum=neg --ho-prim-max=1 --recognize-injectivity=true --ho-elim-leibniz=1 --ho-unif-level=pragmatic-framework --no-max-vars -q \"1|prefer-sos|conjecture-relative-var(1.02,l,f)\" -q \"4|const|conjecture-relative-var(1,s,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-sos|pnrefined(2,1,1,1,2,2,2)\" --select=e-selection7 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=2 --e-auto=true --sine=50 --sine-tolerance=10 --sine-depth-max=5 --sine-depth-min=1 --e-max-derived=64 --e-encode-lambdas=lift --scan-clause-ac=false --prec-gen-fun=invfreq_conj --ord=lambda_kbo --solid-subsumption=true --ignore-orphans=true --e-call-point=0.2")),  (* sh5_noforms.sh *)
+          ((1, 1024, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --max-inferences=4 --ho-unif-max-depth=3 --ho-max-elims=0 --ho-max-app-projections=1 --ho-max-identifications=0 --ho-max-rigid-imitations=2 --ho-unif-level=pragmatic-framework --boolean-reasoning=simpl-only --kbo-weight-fun=freqrank --ext-rules=ext-family --ext-rules-max-depth=2 --ho-prim-enum=eq --ho-prim-max=2 --interpret-bool-funs=false -q \"2|prefer-goals|default\" -q \"8|prefer-sos|conjecture-relative-var(1,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-lambdas|explore\" -q \"1|prefer-non-goals|explore\" -q \"1|prefer-processed|conjecture-relative-var(1,s,f)\" --recognize-injectivity=true --ho-selection-restriction=none --select=ho-selection2 --solve-formulas=true")),  (* sh8_old_zip1.sh *)
+          ((1, 256, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --boolean-reasoning=simpl-only --tptp-def-as-rewrite --rewrite-before-cnf=true --kbo-weight-fun=freqrank -q \"1|prefer-sos|default\" -q \"1|prefer-goals|conjecture-relative-var(1.03,s,f)\" -q \"1|prefer-non-goals|default\" -q \"5|const|conjecture-relative-var(1.01,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|const|conjecture-relative-var(1.05,l,f)\" -q \"1|defer-sos|conjecture-relative-var(1.1,s,f)\" --select=e-selection9 --recognize-injectivity=true --ho-choice-inst=false --ho-selection-restriction=none --sine=50 --sine-tolerance=3 --sine-depth-max=3 --sine-depth-min=1 --eq-encode=true --avatar=eager --sine-trim-implications=true"))],  (* sh5_sh.eqenc.sh *)
      good_max_mono_iters = default_max_mono_iters,
      good_max_new_mono_instances = default_max_new_mono_instances}
   end
@@ -528,7 +537,7 @@
    known_failures = known_szs_status_failures,
    prem_role = prem_role,
    good_slices =
-     K [((1, 256, "mepo"), (format, type_enc,
+     K [((2, 256, "mepo"), (format, type_enc,
       if is_format_higher_order format then keep_lamsN else combsN, uncurried_aliases, ""))],
    good_max_mono_iters = default_max_mono_iters,
    good_max_new_mono_instances = default_max_new_mono_instances}

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Sat Aug 20 21:33:51 2022 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Sat Aug 20 21:34:55 2022 +0200
@@ -70,7 +70,7 @@
    ("try0", "true"),
    ("smt_proofs", "true"),
    ("minimize", "true"),
-   ("slices", string_of_int (6 * Multithreading.max_threads ())),
+   ("slices", string_of_int (12 * Multithreading.max_threads ())),
    ("preplay_timeout", "1")]
 
 val alias_params =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Aug 20 21:33:51 2022 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Aug 20 21:34:55 2022 +0200
@@ -494,9 +494,12 @@
                   (if do_preplay then [string_of_play_outcome play_outcome] else [])
               in
                 one_line_proof_text ctxt 0 one_line_params ^
-                "\n\nIsar proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^
-                Active.sendback_markup_command
-                  (string_of_isar_proof ctxt subgoal subgoal_count isar_proof)
+                (if isar_proofs <> NONE orelse (case play_outcome of Played _ => true | _ => false) then
+                   "\n\nIsar proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^
+                   Active.sendback_markup_command
+                     (string_of_isar_proof ctxt subgoal subgoal_count isar_proof)
+                 else
+                   "")
               end)
           end
       end

--- a/src/HOL/Tools/lin_arith.ML	Sat Aug 20 21:33:51 2022 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Sat Aug 20 21:34:55 2022 +0200
@@ -104,6 +104,15 @@
 val neq_limit = Attrib.setup_config_int \<^binding>\<open>linarith_neq_limit\<close> (K 9);
 val trace = Attrib.setup_config_bool \<^binding>\<open>linarith_trace\<close> (K false);
 
+fun nnf_simpset ctxt =
+  (empty_simpset ctxt
+    |> Simplifier.set_mkeqTrue mk_eq_True
+    |> Simplifier.set_mksimps (mksimps mksimps_pairs))
+  addsimps @{thms imp_conv_disj iff_conv_conj_imp de_Morgan_disj
+    de_Morgan_conj not_all not_ex not_not}
+
+fun prem_nnf_tac ctxt = full_simp_tac (nnf_simpset ctxt)
+
 
 structure LA_Data: LIN_ARITH_DATA =
 struct
@@ -764,6 +773,7 @@
     result
   end;
 
+
 (* takes the i-th subgoal  [| A1; ...; An |] ==> B  to                       *)
 (* An --> ... --> A1 --> B,  performs splitting with the given 'split_thms'  *)
 (* (resulting in a different subgoal P), takes  P  to  ~P ==> False,         *)
@@ -773,16 +783,6 @@
 (* general form  [| Q1; ...; Qm |] ==> False.  Fails if more than            *)
 (* !split_limit splits are possible.                              *)
 
-local
-  fun nnf_simpset ctxt =
-    (empty_simpset ctxt
-      |> Simplifier.set_mkeqTrue mk_eq_True
-      |> Simplifier.set_mksimps (mksimps mksimps_pairs))
-    addsimps [@{thm imp_conv_disj}, @{thm iff_conv_conj_imp}, @{thm de_Morgan_disj},
-      @{thm de_Morgan_conj}, not_all, not_ex, not_not]
-  fun prem_nnf_tac ctxt = full_simp_tac (nnf_simpset ctxt)
-in
-
 fun split_once_tac ctxt split_thms =
   let
     val thy = Proof_Context.theory_of ctxt
@@ -813,8 +813,6 @@
     ]
   end;
 
-end;  (* local *)
-
 (* remove irrelevant premises, then split the i-th subgoal (and all new      *)
 (* subgoals) by using 'split_once_tac' repeatedly.  Beta-eta-normalize new   *)
 (* subgoals and finally attempt to solve them by finding an immediate        *)
@@ -897,16 +895,6 @@
    where the Ai are atomic, i.e. no top-level &, | or EX
 *)
 
-local
-  fun nnf_simpset ctxt =
-    (empty_simpset ctxt
-      |> Simplifier.set_mkeqTrue mk_eq_True
-      |> Simplifier.set_mksimps (mksimps mksimps_pairs))
-    addsimps [@{thm imp_conv_disj}, @{thm iff_conv_conj_imp}, @{thm de_Morgan_disj},
-      @{thm de_Morgan_conj}, @{thm not_all}, @{thm not_ex}, @{thm not_not}];
-  fun prem_nnf_tac ctxt = full_simp_tac (nnf_simpset ctxt);
-in
-
 fun refute_tac ctxt test prep_tac ref_tac =
   let val refute_prems_tac =
         REPEAT_DETERM
@@ -921,8 +909,6 @@
             SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)]
   end;
 
-end;
-
 
 (* arith proof method *)
 
@@ -961,7 +947,7 @@
 val global_setup =
   map_theory_simpset (fn ctxt => ctxt
     addSolver (mk_solver "lin_arith" (add_arith_facts #> Fast_Arith.prems_lin_arith_tac))) #>
-  Attrib.setup \<^binding>\<open>arith_split\<close> (Scan.succeed (Thm.declaration_attribute add_split))
+  Attrib.setup \<^binding>\<open>linarith_split\<close> (Scan.succeed (Thm.declaration_attribute add_split))
     "declaration of split rules for arithmetic procedure" #>
   Method.setup \<^binding>\<open>linarith\<close>
     (Scan.succeed (fn ctxt =>

--- a/src/HOL/Tools/numeral_simprocs.ML	Sat Aug 20 21:33:51 2022 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML	Sat Aug 20 21:34:55 2022 +0200
@@ -166,7 +166,7 @@
   simpset_of (put_simpset HOL_basic_ss \<^context> |> Simplifier.set_term_ord numterm_ord);
 
 (*Maps 1 to Numeral1 so that arithmetic isn't complicated by the abstract 1.*)
-val numeral_syms = [@{thm numeral_One} RS sym];
+val numeral_syms = @{thms numeral_One [symmetric]};
 
 (*Simplify 0+n, n+0, Numeral1*n, n*Numeral1, 1*x, x*1, x/1 *)
 val add_0s =  @{thms add_0_left add_0_right};
@@ -174,57 +174,54 @@
 
 (* For post-simplification of the rhs of simproc-generated rules *)
 val post_simps =
-    [@{thm numeral_One},
-     @{thm add_0_left}, @{thm add_0_right},
-     @{thm mult_zero_left}, @{thm mult_zero_right},
-     @{thm mult_1_left}, @{thm mult_1_right},
-     @{thm mult_minus1}, @{thm mult_minus1_right}]
+    @{thms numeral_One
+      add_0_left add_0_right
+      mult_zero_left mult_zero_right
+      mult_1_left mult_1_right
+      mult_minus1 mult_minus1_right}
 
 val field_post_simps =
-    post_simps @ [@{thm div_0}, @{thm div_by_1}]
+    post_simps @ @{thms div_0 div_by_1}
 
 (*Simplify inverse Numeral1*)
-val inverse_1s = [@{thm inverse_numeral_1}];
+val inverse_1s = @{thms inverse_numeral_1}
 
 (*To perform binary arithmetic.  The "left" rewriting handles patterns
   created by the Numeral_Simprocs, such as 3 * (5 * x). *)
 val simps =
-    [@{thm numeral_One} RS sym] @
-    @{thms add_numeral_left} @
-    @{thms add_neg_numeral_left} @
-    @{thms mult_numeral_left} @
-    @{thms arith_simps} @ @{thms rel_simps};
+    @{thms numeral_One [symmetric]
+      add_numeral_left
+      add_neg_numeral_left
+      mult_numeral_left
+      arith_simps rel_simps}
 
 (*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms
   during re-arrangement*)
 val non_add_simps =
   subtract Thm.eq_thm
-    (@{thms add_numeral_left} @
-     @{thms add_neg_numeral_left} @
-     @{thms numeral_plus_numeral} @
-     @{thms add_neg_numeral_simps}) simps;
-
-(*To evaluate binary negations of coefficients*)
-val minus_simps = [@{thm minus_zero}, @{thm minus_minus}];
+    @{thms add_numeral_left
+       add_neg_numeral_left
+       numeral_plus_numeral
+       add_neg_numeral_simps} simps;
 
 (*To let us treat subtraction as addition*)
-val diff_simps = [@{thm diff_conv_add_uminus}, @{thm minus_add_distrib}, @{thm minus_minus}];
+val diff_simps = @{thms diff_conv_add_uminus minus_add_distrib minus_minus};
 
 (*To let us treat division as multiplication*)
-val divide_simps = [@{thm divide_inverse}, @{thm inverse_mult_distrib}, @{thm inverse_inverse_eq}];
+val divide_simps = @{thms divide_inverse inverse_mult_distrib inverse_inverse_eq};
 
 (*to extract again any uncancelled minuses*)
 val minus_from_mult_simps =
-    [@{thm minus_minus}, @{thm mult_minus_left}, @{thm mult_minus_right}];
+    @{thms minus_minus mult_minus_left mult_minus_right};
 
 (*combine unary minus with numeric literals, however nested within a product*)
 val mult_minus_simps =
-    [@{thm mult.assoc}, @{thm minus_mult_right}, @{thm minus_mult_commute}, @{thm numeral_times_minus_swap}];
+    @{thms mult.assoc minus_mult_right minus_mult_commute numeral_times_minus_swap};
 
 val norm_ss1 =
   simpset_of (put_simpset num_ss \<^context>
     addsimps numeral_syms @ add_0s @ mult_1s @
-    diff_simps @ minus_simps @ @{thms ac_simps})
+    diff_simps @ @{thms minus_zero ac_simps})
 
 val norm_ss2 =
   simpset_of (put_simpset num_ss \<^context>
@@ -232,7 +229,7 @@
 
 val norm_ss3 =
   simpset_of (put_simpset num_ss \<^context>
-    addsimps minus_from_mult_simps @ @{thms ac_simps} @ @{thms ac_simps minus_mult_commute})
+    addsimps minus_from_mult_simps @ @{thms ac_simps minus_mult_commute})
 
 structure CancelNumeralsCommon =
 struct
@@ -249,7 +246,7 @@
     THEN ALLGOALS (simp_tac (put_simpset norm_ss3 ctxt))
 
   val numeral_simp_ss =
-    simpset_of (put_simpset HOL_basic_ss \<^context> addsimps add_0s @ simps)
+    simpset_of (put_simpset HOL_basic_ss \<^context> addsimps simps)
   fun numeral_simp_tac ctxt =
     ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt))
   val simplify_meta_eq = Arith_Data.simplify_meta_eq post_simps
@@ -303,7 +300,7 @@
     THEN ALLGOALS (simp_tac (put_simpset norm_ss3 ctxt))
 
   val numeral_simp_ss =
-    simpset_of (put_simpset HOL_basic_ss \<^context> addsimps add_0s @ simps)
+    simpset_of (put_simpset HOL_basic_ss \<^context> addsimps simps)
   fun numeral_simp_tac ctxt =
     ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt))
   val simplify_meta_eq = Arith_Data.simplify_meta_eq post_simps
@@ -326,7 +323,7 @@
   val trans_tac = trans_tac
 
   val norm_ss1a =
-    simpset_of (put_simpset norm_ss1 \<^context> addsimps inverse_1s @ divide_simps)
+    simpset_of (put_simpset norm_ss1 \<^context> addsimps (inverse_1s @ divide_simps))
   fun norm_tac ctxt =
     ALLGOALS (simp_tac (put_simpset norm_ss1a ctxt))
     THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt))
@@ -334,7 +331,7 @@
 
   val numeral_simp_ss =
     simpset_of (put_simpset HOL_basic_ss \<^context>
-      addsimps add_0s @ simps @ [@{thm add_frac_eq}, @{thm not_False_eq_True}])
+      addsimps (simps @ @{thms add_frac_eq not_False_eq_True}))
   fun numeral_simp_tac ctxt =
     ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt))
   val simplify_meta_eq = Arith_Data.simplify_meta_eq field_post_simps
@@ -386,7 +383,7 @@
   fun numeral_simp_tac ctxt =
     ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt))
   val simplify_meta_eq = Arith_Data.simplify_meta_eq
-    ([@{thm Nat.add_0}, @{thm Nat.add_0_right}] @ post_simps)
+    (@{thms Nat.add_0 Nat.add_0_right} @ post_simps)
   val prove_conv = Arith_Data.prove_conv
 end
 
@@ -588,9 +585,9 @@
 val type_tvar = tvar \<^sort>\<open>type\<close>;
 val geq = cterm_of (Const (\<^const_name>\<open>HOL.eq\<close>, TVar type_tvar --> TVar type_tvar --> \<^typ>\<open>bool\<close>));
 
-val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"}
-val add_frac_num = mk_meta_eq @{thm "add_frac_num"}
-val add_num_frac = mk_meta_eq @{thm "add_num_frac"}
+val add_frac_eq = mk_meta_eq @{thm add_frac_eq}
+val add_frac_num = mk_meta_eq @{thm add_frac_num}
+val add_num_frac = mk_meta_eq @{thm add_num_frac}
 
 fun prove_nz ctxt T t =
   let
@@ -706,35 +703,37 @@
       \<^term>\<open>(a::'a::{field, ord}) / b = c\<close>],
     proc = K proc3}
 
-val ths =
- [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
-  @{thm "divide_numeral_1"},
-  @{thm "div_by_0"}, @{thm div_0},
-  @{thm "divide_divide_eq_left"},
-  @{thm "times_divide_eq_left"}, @{thm "times_divide_eq_right"},
-  @{thm "times_divide_times_eq"},
-  @{thm "divide_divide_eq_right"},
-  @{thm diff_conv_add_uminus}, @{thm "minus_divide_left"},
-  @{thm "add_divide_distrib"} RS sym,
-  @{thm Fields.field_divide_inverse} RS sym, @{thm inverse_divide},
-  Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (Conv.rewr_conv (mk_meta_eq @{thm mult.commute}))))
-  (@{thm Fields.field_divide_inverse} RS sym)]
-
 val field_comp_ss =
   simpset_of
     (put_simpset HOL_basic_ss \<^context>
-      addsimps @{thms "semiring_norm"}
-      addsimps ths addsimps @{thms simp_thms}
+      addsimps @{thms semiring_norm
+        mult_numeral_1
+        mult_numeral_1_right
+        divide_numeral_1
+        div_by_0
+        div_0
+        divide_divide_eq_left
+        times_divide_eq_left
+        times_divide_eq_right
+        times_divide_times_eq
+        divide_divide_eq_right
+        diff_conv_add_uminus
+        minus_divide_left
+        add_divide_distrib [symmetric]
+        Fields.field_divide_inverse [symmetric]
+        inverse_divide
+        divide_inverse_commute [symmetric]
+        simp_thms}
       addsimprocs field_cancel_numeral_factors
       addsimprocs [add_frac_frac_simproc, add_frac_num_simproc, ord_frac_simproc]
-      |> Simplifier.add_cong @{thm "if_weak_cong"})
+      |> Simplifier.add_cong @{thm if_weak_cong})
 
 in
 
 fun field_comp_conv ctxt =
   Simplifier.rewrite (put_simpset field_comp_ss ctxt)
   then_conv
-  Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps [@{thm numeral_One}])
+  Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms numeral_One})
 
 end
 

--- a/src/HOL/ex/Arith_Examples.thy	Sat Aug 20 21:33:51 2022 +0200
+++ b/src/HOL/ex/Arith_Examples.thy	Sat Aug 20 21:34:55 2022 +0200
@@ -98,13 +98,13 @@
   by linarith
 
 lemma "(i::nat) mod 0 = i"
-  using split_mod [of _ _ 0, arith_split]
+  using split_mod [of _ _ 0, linarith_split]
     \<comment> \<open>rule \<^text>\<open>split_mod\<close> is only declared by default for numerals\<close>
   by linarith
 
 lemma "(i::nat) mod 1 = 0"
   (* rule split_mod is only declared by default for numerals *)
-  using split_mod [of _ _ 1, arith_split]
+  using split_mod [of _ _ 1, linarith_split]
     \<comment> \<open>rule \<^text>\<open>split_mod\<close> is only declared by default for numerals\<close>
   by linarith
 
@@ -112,12 +112,12 @@
   by linarith
 
 lemma "(i::int) mod 0 = i"
-  using split_zmod [of _ _ 0, arith_split]
+  using split_zmod [of _ _ 0, linarith_split]
     \<comment> \<open>rule \<^text>\<open>split_zmod\<close> is only declared by default for numerals\<close>
   by linarith
 
 lemma "(i::int) mod 1 = 0"
-  using split_zmod [of _ _ "1", arith_split]
+  using split_zmod [of _ _ "1", linarith_split]
     \<comment> \<open>rule \<^text>\<open>split_zmod\<close> is only declared by default for numerals\<close>
   by linarith