# HG changeset patch
# User desharna
# Date 1662533907 -7200
# Node ID e07d873c18a4f9ff28542ca0a68b5235c35cb5aa
# Parent  c2fd8b88d26272a1e6983674d8ce50b0ab31f79c# Parent  3310317cc4840eeea7de3cb9115fbde225e0d3e7
merged

diff -r c2fd8b88d262 -r e07d873c18a4 CONTRIBUTORS
--- a/CONTRIBUTORS	Fri Sep 02 13:41:55 2022 +0200
+++ b/CONTRIBUTORS	Wed Sep 07 08:58:27 2022 +0200
@@ -6,6 +6,9 @@
 Contributions to this Isabelle version
 --------------------------------------
 
+* August 2022: Norbert Schirmer, Apple
+  Record simproc that sorts update expressions.
+
 * June 2022: Jan van Brügge, TU München
   Strict cardinality bounds for BNFs.
 
diff -r c2fd8b88d262 -r e07d873c18a4 NEWS
--- a/NEWS	Fri Sep 02 13:41:55 2022 +0200
+++ b/NEWS	Wed Sep 07 08:58:27 2022 +0200
@@ -66,6 +66,10 @@
 
 *** HOL ***
 
+* HOL record: new simproc that sorts update expressions, guarded by
+configuration option "record_sort_updates" (default: false). Some
+examples are in theory "HOL-Examples.Records".
+
 * HOL-Algebra: Facts renamed to avoid fact name clashes on interpretation:
 
     is_ring ~> ring_axioms
diff -r c2fd8b88d262 -r e07d873c18a4 etc/options
--- a/etc/options	Fri Sep 02 13:41:55 2022 +0200
+++ b/etc/options	Wed Sep 07 08:58:27 2022 +0200
@@ -133,7 +133,7 @@
   -- "build process output tail shown to user (in lines, 0 = unlimited)"
 
 option profiling : string = "" (standard "time")
-  -- "ML profiling (possible values: time, allocations)"
+  -- "ML profiling (possible values: time, time_thread, allocations)"
 
 option system_log : string = "" (standard "-")
   -- "output for system messages (log file or \"-\" for console progress)"
diff -r c2fd8b88d262 -r e07d873c18a4 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Fri Sep 02 13:41:55 2022 +0200
+++ b/src/HOL/Code_Numeral.thy	Wed Sep 07 08:58:27 2022 +0200
@@ -276,9 +276,11 @@
 declare division_segment_integer.rep_eq [simp]
 
 instance
-  by (standard; transfer)
-    (use mult_le_mono2 [of 1] in \<open>auto simp add: sgn_mult_abs abs_mult sgn_mult abs_mod_less sgn_mod nat_mult_distrib
-     division_segment_mult division_segment_mod intro: div_eqI\<close>)
+  apply (standard; transfer)
+  apply (use mult_le_mono2 [of 1] in \<open>auto simp add: sgn_mult_abs abs_mult sgn_mult abs_mod_less sgn_mod nat_mult_distrib
+     division_segment_mult division_segment_mod\<close>)
+  apply (simp add: division_segment_int_def split: if_splits)
+  done
 
 end
 
diff -r c2fd8b88d262 -r e07d873c18a4 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Fri Sep 02 13:41:55 2022 +0200
+++ b/src/HOL/Divides.thy	Wed Sep 07 08:58:27 2022 +0200
@@ -114,155 +114,6 @@
 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"
-  shows "k div l = (k - l) div l + 1"
-proof -
-  have "k = (k - l) + l" by simp
-  then obtain j where k: "k = j + l" ..
-  with assms show ?thesis by (simp add: div_add_self2)
-qed
-
-lemma mod_pos_geq:
-  fixes k l :: int
-  assumes "0 < l" and "l \<le> k"
-  shows "k mod l = (k - l) mod l"
-proof -
-  have "k = (k - l) + l" by simp
-  then obtain j where k: "k = j + l" ..
-  with assms show ?thesis by simp
-qed
-
-lemma pos_eucl_rel_int_mult_2:
-  assumes "0 \<le> b"
-  assumes "eucl_rel_int a b (q, r)"
-  shows "eucl_rel_int (1 + 2*a) (2*b) (q, 1 + 2*r)"
-  using assms unfolding eucl_rel_int_iff by auto
-
-lemma neg_eucl_rel_int_mult_2:
-  assumes "b \<le> 0"
-  assumes "eucl_rel_int (a + 1) b (q, r)"
-  shows "eucl_rel_int (1 + 2*a) (2*b) (q, 2*r - 1)"
-  using assms unfolding eucl_rel_int_iff by auto
-
-text\<open>computing div by shifting\<close>
-
-lemma pos_zdiv_mult_2: "(0::int) \<le> a ==> (1 + 2*b) div (2*a) = b div a"
-  using pos_eucl_rel_int_mult_2 [OF _ eucl_rel_int]
-  by (rule div_int_unique)
-
-lemma neg_zdiv_mult_2:
-  assumes A: "a \<le> (0::int)" shows "(1 + 2*b) div (2*a) = (b+1) div a"
-  using neg_eucl_rel_int_mult_2 [OF A eucl_rel_int]
-  by (rule div_int_unique)
-
-lemma zdiv_numeral_Bit0 [simp]:
-  "numeral (Num.Bit0 v) div numeral (Num.Bit0 w) =
-    numeral v div (numeral w :: int)"
-  unfolding numeral.simps unfolding mult_2 [symmetric]
-  by (rule div_mult_mult1, simp)
-
-lemma zdiv_numeral_Bit1 [simp]:
-  "numeral (Num.Bit1 v) div numeral (Num.Bit0 w) =
-    (numeral v div (numeral w :: int))"
-  unfolding numeral.simps
-  unfolding mult_2 [symmetric] add.commute [of _ 1]
-  by (rule pos_zdiv_mult_2, simp)
-
-lemma pos_zmod_mult_2:
-  fixes a b :: int
-  assumes "0 \<le> a"
-  shows "(1 + 2 * b) mod (2 * a) = 1 + 2 * (b mod a)"
-  using pos_eucl_rel_int_mult_2 [OF assms eucl_rel_int]
-  by (rule mod_int_unique)
-
-lemma neg_zmod_mult_2:
-  fixes a b :: int
-  assumes "a \<le> 0"
-  shows "(1 + 2 * b) mod (2 * a) = 2 * ((b + 1) mod a) - 1"
-  using neg_eucl_rel_int_mult_2 [OF assms eucl_rel_int]
-  by (rule mod_int_unique)
-
-lemma zmod_numeral_Bit0 [simp]:
-  "numeral (Num.Bit0 v) mod numeral (Num.Bit0 w) =
-    (2::int) * (numeral v mod numeral w)"
-  unfolding numeral_Bit0 [of v] numeral_Bit0 [of w]
-  unfolding mult_2 [symmetric] by (rule mod_mult_mult1)
-
-lemma zmod_numeral_Bit1 [simp]:
-  "numeral (Num.Bit1 v) mod numeral (Num.Bit0 w) =
-    2 * (numeral v mod numeral w) + (1::int)"
-  unfolding numeral_Bit1 [of v] numeral_Bit0 [of w]
-  unfolding mult_2 [symmetric] add.commute [of _ 1]
-  by (rule pos_zmod_mult_2, simp)
-
-  
 subsubsection \<open>Quotients of Signs\<close>
 
 lemma div_eq_minus1: "0 < b \<Longrightarrow> - 1 div b = - 1" for b :: int
@@ -402,6 +253,29 @@
     sgn_mult sgn_1_pos sgn_1_neg sgn_eq_0_iff nonneg1_imp_zdiv_pos_iff * dest: sgn_not_eq_imp)
 qed
 
+lemma
+  fixes a b q r :: int
+  assumes \<open>a = b * q + r\<close> \<open>0 \<le> r\<close> \<open>r < b\<close>
+  shows int_div_pos_eq:
+      \<open>a div b = q\<close> (is ?Q)
+    and int_mod_pos_eq:
+      \<open>a mod b = r\<close> (is ?R)
+proof -
+  from assms have \<open>(a div b, a mod b) = (q, r)\<close>
+    by (cases b q r a rule: euclidean_relationI)
+      (auto simp add: division_segment_int_def ac_simps dvd_add_left_iff dest: zdvd_imp_le)
+  then show ?Q and ?R
+    by simp_all
+qed
+
+lemma int_div_neg_eq:
+  \<open>a div b = q\<close> if \<open>a = b * q + r\<close> \<open>r \<le> 0\<close> \<open>b < r\<close> for a b q r :: int
+  using that int_div_pos_eq [of a \<open>- b\<close> \<open>- q\<close> \<open>- r\<close>] by simp_all
+
+lemma int_mod_neg_eq:
+  \<open>a mod b = r\<close> if \<open>a = b * q + r\<close> \<open>r \<le> 0\<close> \<open>b < r\<close> for a b q r :: int
+  using that int_div_neg_eq [of a b q r] by simp
+
 
 subsubsection \<open>Further properties\<close>
 
@@ -430,21 +304,6 @@
 
 text \<open>Simplify expressions in which div and mod combine numerical constants\<close>
 
-lemma int_div_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a div b = q"
-  by (rule div_int_unique [of a b q r]) (simp add: eucl_rel_int_iff)
-
-lemma int_div_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a div b = q"
-  by (rule div_int_unique [of a b q r],
-    simp add: eucl_rel_int_iff)
-
-lemma int_mod_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a mod b = r"
-  by (rule mod_int_unique [of a b q r],
-    simp add: eucl_rel_int_iff)
-
-lemma int_mod_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a mod b = r"
-  by (rule mod_int_unique [of a b q r],
-    simp add: eucl_rel_int_iff)
-
 lemma abs_div: "(y::int) dvd x \<Longrightarrow> \<bar>x div y\<bar> = \<bar>x\<bar> div \<bar>y\<bar>"
   unfolding dvd_def by (cases "y=0") (auto simp add: abs_mult)
 
@@ -541,6 +400,157 @@
 qed
 
 
+subsubsection \<open>Uniqueness rules\<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 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 unique_quotient:
+  \<open>q = q'\<close> if \<open>eucl_rel_int a b (q, r)\<close> \<open>eucl_rel_int a b (q', r')\<close>
+  apply (rule order_antisym)
+  using that
+   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:
+  \<open>r = r'\<close> if \<open>eucl_rel_int a b (q, r)\<close> \<open>eucl_rel_int a b (q', r')\<close>
+proof -
+  have \<open>q = q'\<close>
+    using that by (blast intro: unique_quotient)
+  then show ?thesis
+    using that by (simp add: eucl_rel_int_iff)
+qed
+
+lemma divmod_int_unique:
+  assumes \<open>eucl_rel_int k l (q, r)\<close>
+  shows div_int_unique: \<open>k div l = q\<close> and mod_int_unique: \<open>k mod l = r\<close>
+  using assms eucl_rel_int [of k l]
+  using unique_quotient [of k l] unique_remainder [of k l]
+  by auto
+
+
+subsubsection \<open>Computing \<open>div\<close> and \<open>mod\<close> with shifting\<close>
+
+lemma div_pos_geq:
+  fixes k l :: int
+  assumes "0 < l" and "l \<le> k"
+  shows "k div l = (k - l) div l + 1"
+proof -
+  have "k = (k - l) + l" by simp
+  then obtain j where k: "k = j + l" ..
+  with assms show ?thesis by (simp add: div_add_self2)
+qed
+
+lemma mod_pos_geq:
+  fixes k l :: int
+  assumes "0 < l" and "l \<le> k"
+  shows "k mod l = (k - l) mod l"
+proof -
+  have "k = (k - l) + l" by simp
+  then obtain j where k: "k = j + l" ..
+  with assms show ?thesis by simp
+qed
+
+lemma pos_eucl_rel_int_mult_2:
+  assumes "0 \<le> b"
+  assumes "eucl_rel_int a b (q, r)"
+  shows "eucl_rel_int (1 + 2*a) (2*b) (q, 1 + 2*r)"
+  using assms unfolding eucl_rel_int_iff by auto
+
+lemma neg_eucl_rel_int_mult_2:
+  assumes "b \<le> 0"
+  assumes "eucl_rel_int (a + 1) b (q, r)"
+  shows "eucl_rel_int (1 + 2*a) (2*b) (q, 2*r - 1)"
+  using assms unfolding eucl_rel_int_iff by auto
+
+text\<open>computing div by shifting\<close>
+
+lemma pos_zdiv_mult_2: "(0::int) \<le> a ==> (1 + 2*b) div (2*a) = b div a"
+  using pos_eucl_rel_int_mult_2 [OF _ eucl_rel_int]
+  by (rule div_int_unique)
+
+lemma neg_zdiv_mult_2:
+  assumes A: "a \<le> (0::int)" shows "(1 + 2*b) div (2*a) = (b+1) div a"
+  using neg_eucl_rel_int_mult_2 [OF A eucl_rel_int]
+  by (rule div_int_unique)
+
+lemma zdiv_numeral_Bit0 [simp]:
+  "numeral (Num.Bit0 v) div numeral (Num.Bit0 w) =
+    numeral v div (numeral w :: int)"
+  unfolding numeral.simps unfolding mult_2 [symmetric]
+  by (rule div_mult_mult1, simp)
+
+lemma zdiv_numeral_Bit1 [simp]:
+  "numeral (Num.Bit1 v) div numeral (Num.Bit0 w) =
+    (numeral v div (numeral w :: int))"
+  unfolding numeral.simps
+  unfolding mult_2 [symmetric] add.commute [of _ 1]
+  by (rule pos_zdiv_mult_2, simp)
+
+lemma pos_zmod_mult_2:
+  fixes a b :: int
+  assumes "0 \<le> a"
+  shows "(1 + 2 * b) mod (2 * a) = 1 + 2 * (b mod a)"
+  using pos_eucl_rel_int_mult_2 [OF assms eucl_rel_int]
+  by (rule mod_int_unique)
+
+lemma neg_zmod_mult_2:
+  fixes a b :: int
+  assumes "a \<le> 0"
+  shows "(1 + 2 * b) mod (2 * a) = 2 * ((b + 1) mod a) - 1"
+  using neg_eucl_rel_int_mult_2 [OF assms eucl_rel_int]
+  by (rule mod_int_unique)
+
+lemma zmod_numeral_Bit0 [simp]:
+  "numeral (Num.Bit0 v) mod numeral (Num.Bit0 w) =
+    (2::int) * (numeral v mod numeral w)"
+  unfolding numeral_Bit0 [of v] numeral_Bit0 [of w]
+  unfolding mult_2 [symmetric] by (rule mod_mult_mult1)
+
+lemma zmod_numeral_Bit1 [simp]:
+  "numeral (Num.Bit1 v) mod numeral (Num.Bit0 w) =
+    2 * (numeral v mod numeral w) + (1::int)"
+  unfolding numeral_Bit1 [of v] numeral_Bit0 [of w]
+  unfolding mult_2 [symmetric] add.commute [of _ 1]
+  by (rule pos_zmod_mult_2, simp)
+
+  
 code_identifier
   code_module Divides \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
 
diff -r c2fd8b88d262 -r e07d873c18a4 src/HOL/Euclidean_Division.thy
--- a/src/HOL/Euclidean_Division.thy	Fri Sep 02 13:41:55 2022 +0200
+++ b/src/HOL/Euclidean_Division.thy	Wed Sep 07 08:58:27 2022 +0200
@@ -605,205 +605,235 @@
 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"
-  assumes is_unit_division_segment [simp]: "is_unit (division_segment a)"
+  assumes euclidean_size_mult: \<open>euclidean_size (a * b) = euclidean_size a * euclidean_size b\<close>
+  fixes division_segment :: \<open>'a \<Rightarrow> 'a\<close>
+  assumes is_unit_division_segment [simp]: \<open>is_unit (division_segment a)\<close>
     and division_segment_mult:
-    "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> division_segment (a * b) = division_segment a * division_segment b"
+    \<open>a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> division_segment (a * b) = division_segment a * division_segment b\<close>
     and division_segment_mod:
-    "b \<noteq> 0 \<Longrightarrow> \<not> b dvd a \<Longrightarrow> division_segment (a mod b) = division_segment b"
+    \<open>b \<noteq> 0 \<Longrightarrow> \<not> b dvd a \<Longrightarrow> division_segment (a mod b) = division_segment b\<close>
   assumes div_bounded:
-    "b \<noteq> 0 \<Longrightarrow> division_segment r = division_segment b
+    \<open>b \<noteq> 0 \<Longrightarrow> division_segment r = division_segment b
     \<Longrightarrow> euclidean_size r < euclidean_size b
-    \<Longrightarrow> (q * b + r) div b = q"
+    \<Longrightarrow> (q * b + r) div b = q\<close>
 begin
 
 lemma division_segment_not_0 [simp]:
-  "division_segment a \<noteq> 0"
-  using is_unit_division_segment [of a] is_unitE [of "division_segment a"] by blast
-
-lemma divmod_cases [case_names divides remainder by0]:
-  obtains 
-    (divides) q where "b \<noteq> 0"
-      and "a div b = q"
-      and "a mod b = 0"
-      and "a = q * b"
-  | (remainder) q r where "b \<noteq> 0"
-      and "division_segment r = division_segment b"
-      and "euclidean_size r < euclidean_size b"
-      and "r \<noteq> 0"
-      and "a div b = q"
-      and "a mod b = r"
-      and "a = q * b + r"
-  | (by0) "b = 0"
-proof (cases "b = 0")
+  \<open>division_segment a \<noteq> 0\<close>
+  using is_unit_division_segment [of a] is_unitE [of \<open>division_segment a\<close>] by blast
+
+lemma euclidean_relationI [case_names by0 divides euclidean_relation]:
+  \<open>(a div b, a mod b) = (q, r)\<close>
+    if by0: \<open>b = 0 \<Longrightarrow> q = 0 \<and> r = a\<close>
+    and divides: \<open>b \<noteq> 0 \<Longrightarrow> b dvd a \<Longrightarrow> r = 0 \<and> a = q * b\<close>
+    and euclidean_relation: \<open>b \<noteq> 0 \<Longrightarrow> \<not> b dvd a \<Longrightarrow> division_segment r = division_segment b
+      \<and> euclidean_size r < euclidean_size b \<and> a = q * b + r\<close>
+proof (cases \<open>b = 0\<close>)
   case True
-  then show thesis
-  by (rule by0)
+  with by0 show ?thesis
+    by simp
 next
   case False
-  show thesis
-  proof (cases "b dvd a")
+  show ?thesis
+  proof (cases \<open>b dvd a\<close>)
     case True
-    then obtain q where "a = b * q" ..
     with \<open>b \<noteq> 0\<close> divides
-    show thesis
-      by (simp add: ac_simps)
+    show ?thesis
+      by simp
   next
     case False
-    then have "a mod b \<noteq> 0"
-      by (simp add: mod_eq_0_iff_dvd)
-    moreover from \<open>b \<noteq> 0\<close> \<open>\<not> b dvd a\<close> have "division_segment (a mod b) = division_segment b"
-      by (rule division_segment_mod)
-    moreover have "euclidean_size (a mod b) < euclidean_size b"
-      using \<open>b \<noteq> 0\<close> by (rule mod_size_less)
-    moreover have "a = a div b * b + a mod b"
+    with \<open>b \<noteq> 0\<close> euclidean_relation
+    have \<open>division_segment r = division_segment b\<close>
+      \<open>euclidean_size r < euclidean_size b\<close> \<open>a = q * b + r\<close>
+      by simp_all
+    from \<open>b \<noteq> 0\<close> \<open>division_segment r = division_segment b\<close>
+      \<open>euclidean_size r < euclidean_size b\<close>
+    have \<open>(q * b + r) div b = q\<close>
+      by (rule div_bounded)
+    with \<open>a = q * b + r\<close>
+    have \<open>q = a div b\<close>
+      by simp
+    from \<open>a = q * b + r\<close>
+    have \<open>a div b * b + a mod b = q * b + r\<close>
       by (simp add: div_mult_mod_eq)
-    ultimately show thesis
-      using \<open>b \<noteq> 0\<close> by (blast intro!: remainder)
+    with \<open>q = a div b\<close>
+    have \<open>q * b + a mod b = q * b + r\<close>
+      by simp
+    then have \<open>r = a mod b\<close>
+      by simp
+    with \<open>q = a div b\<close>
+    show ?thesis
+      by simp
   qed
 qed
 
-lemma div_eqI:
-  "a div b = q" if "b \<noteq> 0" "division_segment r = division_segment b"
-    "euclidean_size r < euclidean_size b" "q * b + r = a"
-proof -
-  from that have "(q * b + r) div b = q"
-    by (auto intro: div_bounded)
-  with that show ?thesis
-    by simp
-qed
-
-lemma mod_eqI:
-  "a mod b = r" if "b \<noteq> 0" "division_segment r = division_segment b"
-    "euclidean_size r < euclidean_size b" "q * b + r = a" 
-proof -
-  from that have "a div b = q"
-    by (rule div_eqI)
-  moreover have "a div b * b + a mod b = a"
-    by (fact div_mult_mod_eq)
-  ultimately have "a div b * b + a mod b = a div b * b + r"
-    using \<open>q * b + r = a\<close> by simp
-  then show ?thesis
-    by simp
-qed
-
 subclass euclidean_semiring_cancel
 proof
-  show "(a + c * b) div b = c + a div b" if "b \<noteq> 0" for a b c
-  proof (cases a b rule: divmod_cases)
+  fix a b c
+  assume \<open>b \<noteq> 0\<close>
+  have \<open>((a + c * b) div b, (a + c * b) mod b) = (c + a div b, a mod b)\<close>
+  proof (cases b \<open>c + a div b\<close> \<open>a mod b\<close> \<open>a + c * b\<close> rule: euclidean_relationI)
     case by0
-    with \<open>b \<noteq> 0\<close> show ?thesis
+    with \<open>b \<noteq> 0\<close>
+    show ?case
+      by simp
+  next
+    case divides
+    then show ?case
+      by (simp add: algebra_simps dvd_add_left_iff)
+  next
+    case euclidean_relation
+    then have \<open>\<not> b dvd a\<close>
+      by (simp add: dvd_add_left_iff)
+    have \<open>a mod b + (b * c + b * (a div b)) = b * c + ((a div b) * b + a mod b)\<close>
+      by (simp add: ac_simps)
+    with \<open>b \<noteq> 0\<close> have *: \<open>a mod b + (b * c + b * (a div b)) = b * c + a\<close>
+      by (simp add: div_mult_mod_eq)
+    from \<open>\<not> b dvd a\<close> euclidean_relation show ?case
+      by (simp_all add: algebra_simps division_segment_mod mod_size_less *)
+  qed
+  then show \<open>(a + c * b) div b = c + a div b\<close>
+    by simp
+next
+  fix a b c
+  assume \<open>c \<noteq> 0\<close>
+  have \<open>((c * a) div (c * b), (c * a) mod (c * b)) = (a div b, c * (a mod b))\<close>
+  proof (cases \<open>c * b\<close> \<open>a div b\<close> \<open>c * (a mod b)\<close> \<open>c * a\<close> rule: euclidean_relationI)
+    case by0
+    with \<open>c \<noteq> 0\<close> show ?case
       by simp
   next
-    case (divides q)
-    then show ?thesis
-      by (simp add: ac_simps)
+    case divides
+    then show ?case
+      by (auto simp add: algebra_simps)
   next
-    case (remainder q r)
-    then show ?thesis
-      by (auto intro: div_eqI simp add: algebra_simps)
+    case euclidean_relation
+    then have \<open>b \<noteq> 0\<close> \<open>a mod b \<noteq> 0\<close>
+      by (simp_all add: mod_eq_0_iff_dvd)
+    have \<open>c * (a mod b) + b * (c * (a div b)) = c * ((a div b) * b + a mod b)\<close>
+      by (simp add: algebra_simps)
+    with \<open>b \<noteq> 0\<close> have *: \<open>c * (a mod b) + b * (c * (a div b)) = c * a\<close>
+      by (simp add: div_mult_mod_eq)
+    from \<open>b \<noteq> 0\<close> \<open>c \<noteq> 0\<close> have \<open>euclidean_size c * euclidean_size (a mod b)
+      < euclidean_size c * euclidean_size b\<close>
+      using mod_size_less [of b a] by simp
+    with euclidean_relation \<open>b \<noteq> 0\<close> \<open>a mod b \<noteq> 0\<close> show ?case
+      by (simp add: algebra_simps division_segment_mult division_segment_mod euclidean_size_mult *)
   qed
+  then show \<open>(c * a) div (c * b) = a div b\<close>
+    by simp
+qed
+
+lemma div_eq_0_iff:
+  \<open>a div b = 0 \<longleftrightarrow> euclidean_size a < euclidean_size b \<or> b = 0\<close> (is "_ \<longleftrightarrow> ?P")
+  if \<open>division_segment a = division_segment b\<close>
+proof (cases \<open>a = 0 \<or> b = 0\<close>)
+  case True
+  then show ?thesis by auto
 next
-  show"(c * a) div (c * b) = a div b" if "c \<noteq> 0" for a b c
-  proof (cases a b rule: divmod_cases)
-    case by0
-    then show ?thesis
+  case False
+  then have \<open>a \<noteq> 0\<close> \<open>b \<noteq> 0\<close>
+    by simp_all
+  have \<open>a div b = 0 \<longleftrightarrow> euclidean_size a < euclidean_size b\<close>
+  proof
+    assume \<open>a div b = 0\<close>
+    then have \<open>a mod b = a\<close>
+      using div_mult_mod_eq [of a b] by simp
+    with \<open>b \<noteq> 0\<close> mod_size_less [of b a]
+    show \<open>euclidean_size a < euclidean_size b\<close>
       by simp
   next
-    case (divides q)
-    with \<open>c \<noteq> 0\<close> show ?thesis
-      by (simp add: mult.left_commute [of c])
-  next
-    case (remainder q r)
-    from \<open>b \<noteq> 0\<close> \<open>c \<noteq> 0\<close> have "b * c \<noteq> 0"
+    assume \<open>euclidean_size a < euclidean_size b\<close>
+    have \<open>(a div b, a mod b) = (0, a)\<close>
+    proof (cases b 0 a a rule: euclidean_relationI)
+      case by0
+      show ?case
+        by simp
+    next
+      case divides
+      with \<open>euclidean_size a < euclidean_size b\<close> show ?case
+        using dvd_imp_size_le [of b a] \<open>a \<noteq> 0\<close> by simp
+    next
+      case euclidean_relation
+      with \<open>euclidean_size a < euclidean_size b\<close> that
+      show ?case
+        by simp
+    qed
+    then show \<open>a div b = 0\<close>
       by simp
-    from remainder \<open>c \<noteq> 0\<close>
-    have "division_segment (r * c) = division_segment (b * c)"
-      and "euclidean_size (r * c) < euclidean_size (b * c)"
-      by (simp_all add: division_segment_mult division_segment_mod euclidean_size_mult)
-    with remainder show ?thesis
-      by (auto intro!: div_eqI [of _ "c * (a mod b)"] simp add: algebra_simps)
-        (use \<open>b * c \<noteq> 0\<close> in simp)
   qed
+  with \<open>b \<noteq> 0\<close> show ?thesis
+    by simp
 qed
 
 lemma div_mult1_eq:
-  "(a * b) div c = a * (b div c) + a * (b mod c) div c"
-proof (cases "a * (b mod c)" c rule: divmod_cases)
-  case (divides q)
-  have "a * b = a * (b div c * c + b mod c)"
-    by (simp add: div_mult_mod_eq)
-  also have "\<dots> = (a * (b div c) + q) * c"
-    using divides by (simp add: algebra_simps)
-  finally have "(a * b) div c = \<dots> div c"
-    by simp
-  with divides show ?thesis
-    by simp
-next
-  case (remainder q r)
-  from remainder(1-3) show ?thesis
-  proof (rule div_eqI)
-    have "a * b = a * (b div c * c + b mod c)"
-      by (simp add: div_mult_mod_eq)
-    also have "\<dots> = a * c * (b div c) + q * c + r"
-      using remainder by (simp add: algebra_simps)
-    finally show "(a * (b div c) + a * (b mod c) div c) * c + r = a * b"
-      using remainder(5-7) by (simp add: algebra_simps)
+  \<open>(a * b) div c = a * (b div c) + a * (b mod c) div c\<close>
+proof -
+  have *: \<open>(a * b) mod c + (a * (c * (b div c)) + c * (a * (b mod c) div c)) = a * b\<close> (is \<open>?A + (?B + ?C) = _\<close>)
+  proof -
+    have \<open>?A = a * (b mod c) mod c\<close>
+      by (simp add: mod_mult_right_eq)
+    then have \<open>?C + ?A = a * (b mod c)\<close>
+      by (simp add: mult_div_mod_eq)
+    then have \<open>?B + (?C + ?A) = a * (c * (b div c) + (b mod c))\<close>
+      by (simp add: algebra_simps)
+    also have \<open>\<dots> = a * b\<close>
+      by (simp add: mult_div_mod_eq)
+    finally show ?thesis
+      by (simp add: algebra_simps)
   qed
-next
-  case by0
+  have \<open>((a * b) div c, (a * b) mod c) = (a * (b div c) + a * (b mod c) div c, (a * b) mod c)\<close>
+  proof (cases c \<open>a * (b div c) + a * (b mod c) div c\<close> \<open>(a * b) mod c\<close> \<open>a * b\<close> rule: euclidean_relationI)
+    case by0
+    then show ?case by simp
+  next
+    case divides
+    with * show ?case
+      by (simp add: algebra_simps)
+  next
+    case euclidean_relation
+    with * show ?case
+      by (simp add: division_segment_mod mod_size_less algebra_simps)
+  qed
   then show ?thesis
     by simp
 qed
 
 lemma div_add1_eq:
-  "(a + b) div c = a div c + b div c + (a mod c + b mod c) div c"
-proof (cases "a mod c + b mod c" c rule: divmod_cases)
-  case (divides q)
-  have "a + b = (a div c * c + a mod c) + (b div c * c + b mod c)"
-    using mod_mult_div_eq [of a c] mod_mult_div_eq [of b c] by (simp add: ac_simps)
-  also have "\<dots> = (a div c + b div c) * c + (a mod c + b mod c)"
-    by (simp add: algebra_simps)
-  also have "\<dots> = (a div c + b div c + q) * c"
-    using divides by (simp add: algebra_simps)
-  finally have "(a + b) div c = (a div c + b div c + q) * c div c"
-    by simp
-  with divides show ?thesis
-    by simp
-next
-  case (remainder q r)
-  from remainder(1-3) show ?thesis
-  proof (rule div_eqI)
-    have "(a div c + b div c + q) * c + r + (a mod c + b mod c) =
-        (a div c * c + a mod c) + (b div c * c + b mod c) + q * c + r"
+  \<open>(a + b) div c = a div c + b div c + (a mod c + b mod c) div c\<close>
+proof -
+  have *: \<open>(a + b) mod c + (c * (a div c) + (c * (b div c) + c * ((a mod c + b mod c) div c))) = a + b\<close>
+    (is \<open>?A + (?B + (?C + ?D)) = _\<close>)
+  proof -
+    have \<open>?A + (?B + (?C + ?D)) = ?A + ?D + (?B + ?C)\<close>
+      by (simp add: ac_simps)
+    also have \<open>?A + ?D = (a mod c + b mod c) mod c + ?D\<close>
+      by (simp add: mod_add_eq)
+    also have \<open>\<dots> = a mod c + b mod c\<close>
+      by (simp add: mod_mult_div_eq)
+    finally have \<open>?A + (?B + (?C + ?D)) = (a mod c + ?B) + (b mod c + ?C)\<close>
+      by (simp add: ac_simps)
+    then show ?thesis
+      by (simp add: mod_mult_div_eq)
+  qed
+  have \<open>((a + b) div c, (a + b) mod c) = (a div c + b div c + (a mod c + b mod c) div c, (a + b) mod c)\<close>
+  proof (cases c \<open>a div c + b div c + (a mod c + b mod c) div c\<close> \<open>(a + b) mod c\<close> \<open>a + b\<close> rule: euclidean_relationI)
+    case by0
+    then show ?case
+      by simp
+  next
+    case divides
+    with * show ?case
       by (simp add: algebra_simps)
-    also have "\<dots> = a + b + (a mod c + b mod c)"
-      by (simp add: div_mult_mod_eq remainder) (simp add: ac_simps)
-    finally show "(a div c + b div c + (a mod c + b mod c) div c) * c + r = a + b"
-      using remainder by simp
+  next
+    case euclidean_relation
+    with * show ?case
+      by (simp add: division_segment_mod mod_size_less algebra_simps)
   qed
-next
-  case by0
   then show ?thesis
     by simp
 qed
 
-lemma div_eq_0_iff:
-  "a div b = 0 \<longleftrightarrow> euclidean_size a < euclidean_size b \<or> b = 0" (is "_ \<longleftrightarrow> ?P")
-  if "division_segment a = division_segment b"
-proof
-  assume ?P
-  with that show "a div b = 0"
-    by (cases "b = 0") (auto intro: div_eqI)
-next
-  assume "a div b = 0"
-  then have "a mod b = a"
-    using div_mult_mod_eq [of a b] by simp
-  with mod_size_less [of b a] show ?P
-    by auto
-qed
-
 end
 
 class unique_euclidean_ring = euclidean_ring + unique_euclidean_semiring
@@ -819,19 +849,19 @@
 instantiation nat :: normalization_semidom
 begin
 
-definition normalize_nat :: "nat \<Rightarrow> nat"
-  where [simp]: "normalize = (id :: nat \<Rightarrow> nat)"
-
-definition unit_factor_nat :: "nat \<Rightarrow> nat"
-  where "unit_factor n = (if n = 0 then 0 else 1 :: nat)"
+definition normalize_nat :: \<open>nat \<Rightarrow> nat\<close>
+  where [simp]: \<open>normalize = (id :: nat \<Rightarrow> nat)\<close>
+
+definition unit_factor_nat :: \<open>nat \<Rightarrow> nat\<close>
+  where \<open>unit_factor n = of_bool (n > 0)\<close> for n :: nat
 
 lemma unit_factor_simps [simp]:
-  "unit_factor 0 = (0::nat)"
-  "unit_factor (Suc n) = 1"
+  \<open>unit_factor 0 = (0::nat)\<close>
+  \<open>unit_factor (Suc n) = 1\<close>
   by (simp_all add: unit_factor_nat_def)
 
-definition divide_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-  where "m div n = (if n = 0 then 0 else Max {k::nat. k * n \<le> m})"
+definition divide_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close>
+  where \<open>m div n = (if n = 0 then 0 else Max {k. k * n \<le> m})\<close> for m n :: nat
 
 instance
   by standard (auto simp add: divide_nat_def ac_simps unit_factor_nat_def intro: Max_eqI)
@@ -853,14 +883,14 @@
 instantiation nat :: unique_euclidean_semiring
 begin
 
-definition euclidean_size_nat :: "nat \<Rightarrow> nat"
-  where [simp]: "euclidean_size_nat = id"
-
-definition division_segment_nat :: "nat \<Rightarrow> nat"
-  where [simp]: "division_segment_nat n = 1"
-
-definition modulo_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-  where "m mod n = m - (m div n * (n::nat))"
+definition euclidean_size_nat :: \<open>nat \<Rightarrow> nat\<close>
+  where [simp]: \<open>euclidean_size_nat = id\<close>
+
+definition division_segment_nat :: \<open>nat \<Rightarrow> nat\<close>
+  where [simp]: \<open>division_segment n = 1\<close> for n :: nat
+
+definition modulo_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close>
+  where \<open>m mod n = m - (m div n * n)\<close> for m n :: nat
 
 instance proof
   fix m n :: nat
@@ -938,12 +968,60 @@
 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>)
+  \<open>m div n = q\<close> if \<open>n * q \<le> m\<close> and \<open>m < n * Suc q\<close> for m n q :: nat
+proof -
+  have \<open>(m div n, m mod n) = (q, m - n * q)\<close>
+  proof (cases n q \<open>m - n * q\<close>  m rule: euclidean_relationI)
+    case by0
+    with that show ?case
+      by simp
+  next
+    case divides
+    from \<open>n dvd m\<close> obtain s where \<open>m = n * s\<close> ..
+    with \<open>n \<noteq> 0\<close> that have \<open>s < Suc q\<close>
+      by (simp only: mult_less_cancel1)
+    with \<open>m = n * s\<close> \<open>n \<noteq> 0\<close> that have \<open>q = s\<close>
+      by simp
+    with \<open>m = n * s\<close> show ?case
+      by (simp add: ac_simps)
+  next
+    case euclidean_relation
+    with that show ?case
+      by (simp add: ac_simps)
+  qed
+  then show ?thesis
+    by simp
+qed
 
 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>)
+  \<open>m mod n = r\<close> if \<open>r < n\<close> and \<open>r \<le> m\<close> and \<open>n dvd m - r\<close> for m n r :: nat
+proof -
+  have \<open>(m div n, m mod n) = ((m - r) div n, r)\<close>
+  proof (cases n \<open>(m - r) div n\<close> r  m rule: euclidean_relationI)
+    case by0
+    with that show ?case
+      by simp
+  next
+    case divides
+    from that dvd_minus_add [of r \<open>m\<close> 1 n]
+    have \<open>n dvd m + (n - r)\<close>
+      by simp
+    with divides have \<open>n dvd n - r\<close>
+      by (simp add: dvd_add_right_iff)
+    then have \<open>n \<le> n - r\<close>
+      by (rule dvd_imp_le) (use \<open>r < n\<close> in simp)
+    with \<open>n \<noteq> 0\<close> have \<open>r = 0\<close>
+      by simp
+    with \<open>n \<noteq> 0\<close> that show ?case
+      by simp
+  next
+    case euclidean_relation
+    with that show ?case
+      by (simp add: ac_simps)
+  qed
+  then show ?thesis
+    by simp
+qed
 
 text \<open>Tool support\<close>
 
@@ -1029,7 +1107,7 @@
   div_less [simp]: "m div n = 0"
   and mod_less [simp]: "m mod n = m"
   if "m < n" for m n :: nat
-  using that by (auto intro: div_eqI mod_eqI) 
+  using that by (auto intro: div_nat_eqI mod_nat_eqI)
  
 lemma split_div:
   \<open>P (m div n) \<longleftrightarrow>
@@ -1176,54 +1254,43 @@
   "Suc 0 mod n = of_bool (n \<noteq> Suc 0)"
   by (cases n) simp_all
 
-context
-  fixes m n q :: nat
-begin
-
-private lemma eucl_rel_mult2:
-  "m mod n + n * (m div n mod q) < n * q"
-  if "n > 0" and "q > 0"
+lemma div_mult2_eq:
+    \<open>m div (n * q) = (m div n) div q\<close> (is ?Q)
+  and mod_mult2_eq:
+    \<open>m mod (n * q) = n * (m div n mod q) + m mod n\<close> (is ?R)
+  for m n q :: nat
 proof -
-  from \<open>n > 0\<close> have "m mod n < n"
-    by (rule mod_less_divisor)
-  from \<open>q > 0\<close> have "m div n mod q < q"
-    by (rule mod_less_divisor)
-  then obtain s where "q = Suc (m div n mod q + s)"
-    by (blast dest: less_imp_Suc_add)
-  moreover have "m mod n + n * (m div n mod q) < n * Suc (m div n mod q + s)"
-    using \<open>m mod n < n\<close> by (simp add: add_mult_distrib2)
-  ultimately show ?thesis
-    by simp
+  have \<open>(m div (n * q), m mod (n * q)) = ((m div n) div q, n * (m div n mod q) + m mod n)\<close>
+  proof (cases \<open>n * q\<close> \<open>(m div n) div q\<close> \<open>n * (m div n mod q) + m mod n\<close> m rule: euclidean_relationI)
+    case by0
+    then show ?case
+      by auto
+  next
+    case divides
+    from \<open>n * q dvd m\<close> obtain t where \<open>m = n * q * t\<close> ..
+    with \<open>n * q \<noteq> 0\<close> show ?case
+      by (simp add: algebra_simps)
+  next
+    case euclidean_relation
+    then have \<open>n > 0\<close> \<open>q > 0\<close>
+      by simp_all
+    from \<open>n > 0\<close> have \<open>m mod n < n\<close>
+      by (rule mod_less_divisor)
+    from \<open>q > 0\<close> have \<open>m div n mod q < q\<close>
+      by (rule mod_less_divisor)
+    then obtain s where \<open>q = Suc (m div n mod q + s)\<close>
+      by (blast dest: less_imp_Suc_add)
+    moreover have \<open>m mod n + n * (m div n mod q) < n * Suc (m div n mod q + s)\<close>
+      using \<open>m mod n < n\<close> by (simp add: add_mult_distrib2)
+    ultimately have \<open>m mod n + n * (m div n mod q) < n * q\<close>
+      by simp
+    then show ?case
+      by (simp add: algebra_simps flip: add_mult_distrib2)
+  qed
+  then show ?Q and ?R
+    by simp_all
 qed
 
-lemma div_mult2_eq:
-  "m div (n * q) = (m div n) div q"
-proof (cases "n = 0 \<or> q = 0")
-  case True
-  then show ?thesis
-    by auto
-next
-  case False
-  with eucl_rel_mult2 show ?thesis
-    by (auto intro: div_eqI [of _ "n * (m div n mod q) + m mod n"]
-      simp add: algebra_simps add_mult_distrib2 [symmetric])
-qed
-
-lemma mod_mult2_eq:
-  "m mod (n * q) = n * (m div n mod q) + m mod n"
-proof (cases "n = 0 \<or> q = 0")
-  case True
-  then show ?thesis
-    by auto
-next
-  case False
-  with eucl_rel_mult2 show ?thesis
-    by (auto intro: mod_eqI [of _ _ "(m div n) div q"]
-      simp add: algebra_simps add_mult_distrib2 [symmetric])
-qed
-
-end
-
 lemma div_le_mono:
   "m div k \<le> n div k" if "m \<le> n" for m n k :: nat
 proof -
@@ -1864,42 +1931,54 @@
   using div_mult_mod_eq [of 1 "2 ^ n"] by auto
 
 lemma div_mult2_eq':
-  "a div (of_nat m * of_nat n) = a div of_nat m div of_nat n"
-proof (cases a "of_nat m * of_nat n" rule: divmod_cases)
-  case (divides q)
-  then show ?thesis
-    using nonzero_mult_div_cancel_right [of "of_nat m" "q * of_nat n"]
-    by (simp add: ac_simps)
-next
-  case (remainder q r)
-  then have "division_segment r = 1"
-    using division_segment_of_nat [of "m * n"] by simp
-  with division_segment_euclidean_size [of r]
-  have "of_nat (euclidean_size r) = r"
-    by simp
-  have "a mod (of_nat m * of_nat n) div (of_nat m * of_nat n) = 0"
-    by simp
-  with remainder(6) have "r div (of_nat m * of_nat n) = 0"
-    by simp
-  with \<open>of_nat (euclidean_size r) = r\<close>
-  have "of_nat (euclidean_size r) div (of_nat m * of_nat n) = 0"
-    by simp
-  then have "of_nat (euclidean_size r div (m * n)) = 0"
-    by (simp add: of_nat_div)
-  then have "of_nat (euclidean_size r div m div n) = 0"
-    by (simp add: div_mult2_eq)
-  with \<open>of_nat (euclidean_size r) = r\<close> have "r div of_nat m div of_nat n = 0"
-    by (simp add: of_nat_div)
-  with remainder(1)
-  have "q = (r div of_nat m + q * of_nat n * of_nat m div of_nat m) div of_nat n"
-    by simp
-  with remainder(5) remainder(7) show ?thesis
-    using div_plus_div_distrib_dvd_right [of "of_nat m" "q * (of_nat m * of_nat n)" r]
-    by (simp add: ac_simps)
-next
-  case by0
+  \<open>a div (of_nat m * of_nat n) = a div of_nat m div of_nat n\<close>
+proof (cases \<open>m = 0 \<or> n = 0\<close>)
+  case True
   then show ?thesis
     by auto
+next
+  case False
+  then have \<open>m > 0\<close> \<open>n > 0\<close>
+    by simp_all
+  show ?thesis
+  proof (cases \<open>of_nat m * of_nat n dvd a\<close>)
+    case True
+    then obtain b where \<open>a = (of_nat m * of_nat n) * b\<close> ..
+    then have \<open>a = of_nat m * (of_nat n * b)\<close>
+      by (simp add: ac_simps)
+    then show ?thesis
+      by simp
+  next
+    case False
+    define q where \<open>q = a div (of_nat m * of_nat n)\<close>
+    define r where \<open>r = a mod (of_nat m * of_nat n)\<close>
+    from \<open>m > 0\<close> \<open>n > 0\<close> \<open>\<not> of_nat m * of_nat n dvd a\<close> r_def have "division_segment r = 1"
+      using division_segment_of_nat [of "m * n"] by (simp add: division_segment_mod)
+    with division_segment_euclidean_size [of r]
+    have "of_nat (euclidean_size r) = r"
+      by simp
+    have "a mod (of_nat m * of_nat n) div (of_nat m * of_nat n) = 0"
+      by simp
+    with \<open>m > 0\<close> \<open>n > 0\<close> r_def have "r div (of_nat m * of_nat n) = 0"
+      by simp
+    with \<open>of_nat (euclidean_size r) = r\<close>
+    have "of_nat (euclidean_size r) div (of_nat m * of_nat n) = 0"
+      by simp
+    then have "of_nat (euclidean_size r div (m * n)) = 0"
+      by (simp add: of_nat_div)
+    then have "of_nat (euclidean_size r div m div n) = 0"
+      by (simp add: div_mult2_eq)
+    with \<open>of_nat (euclidean_size r) = r\<close> have "r div of_nat m div of_nat n = 0"
+      by (simp add: of_nat_div)
+    with \<open>m > 0\<close> \<open>n > 0\<close> q_def
+    have "q = (r div of_nat m + q * of_nat n * of_nat m div of_nat m) div of_nat n"
+      by simp
+    moreover have \<open>a = q * (of_nat m * of_nat n) + r\<close>
+      by (simp add: q_def r_def div_mult_mod_eq)
+    ultimately show \<open>a div (of_nat m * of_nat n) = a div of_nat m div of_nat n\<close>
+      using q_def [symmetric] div_plus_div_distrib_dvd_right [of \<open>of_nat m\<close> \<open>q * (of_nat m * of_nat n)\<close> r]
+      by (simp add: ac_simps)
+  qed
 qed
 
 lemma mod_mult2_eq':
@@ -2033,31 +2112,45 @@
   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>)
+  \<open>k div l = - 1\<close> if \<open>0 < k\<close> and \<open>k + l \<le> 0\<close> for k l :: int
+proof (cases \<open>l dvd k\<close>)
   case True
-  with that show ?thesis
-    by (simp add: divide_int_def)
+  then obtain j where \<open>k = l * j\<close> ..
+  from that have \<open>l < 0\<close>
+    by simp
+  with \<open>k = l * j\<close> \<open>0 < k\<close> have \<open>j \<le> - 1\<close>
+    by (simp add: zero_less_mult_iff)
+  moreover from \<open>k + l \<le> 0\<close> \<open>k = l * j\<close> have \<open>l * (j + 1) \<le> 0\<close>
+    by (simp add: algebra_simps)
+  with \<open>l < 0\<close> have \<open>- 1 \<le> j\<close>
+    by (simp add: mult_le_0_iff)
+  ultimately have \<open>j = - 1\<close>
+    by (rule order.antisym)
+  with \<open>k = l * j\<close> \<open>l < 0\<close> show ?thesis
+    by (simp add: dvd_neg_div)
 next
   case False
-  show ?thesis
-    apply (rule div_eqI [of _ "k + l"])
-    using False that apply (simp_all add: division_segment_int_def)
-    done
+  have \<open>k + l < 0\<close>
+  proof (rule ccontr)
+    assume \<open>\<not> k + l < 0\<close>
+    with \<open>k + l \<le> 0\<close> have \<open>k + l = 0\<close>
+      by simp
+    then have \<open>k = - l\<close>
+      by simp
+    then have \<open>l dvd k\<close>
+      by simp
+    with \<open>\<not> l dvd k\<close> show False ..
+  qed
+  with that \<open>\<not> l dvd k\<close> show ?thesis
+    by (simp add: div_eq_div_abs [of k l])
 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
+  \<open>k mod l = k + l\<close> if \<open>0 < k\<close> and \<open>k + l \<le> 0\<close> for k l :: int
+proof -
+  from that have \<open>k mod l = k div l * l + k mod l + l\<close>
+    by (simp add: div_pos_neg_trivial)
+  then show ?thesis by simp
 qed
 
 text \<open>There is neither \<open>div_neg_pos_trivial\<close> nor \<open>mod_neg_pos_trivial\<close>
diff -r c2fd8b88d262 -r e07d873c18a4 src/HOL/Examples/Records.thy
--- a/src/HOL/Examples/Records.thy	Fri Sep 02 13:41:55 2022 +0200
+++ b/src/HOL/Examples/Records.thy	Wed Sep 07 08:58:27 2022 +0200
@@ -1,6 +1,7 @@
 (*  Title:      HOL/Examples/Records.thy
     Author:     Wolfgang Naraschewski, TU Muenchen
     Author:     Norbert Schirmer, TU Muenchen
+    Author:     Norbert Schirmer, Apple, 2022
     Author:     Markus Wenzel, TU Muenchen
 *)
 
@@ -294,8 +295,72 @@
   by the following lemma.\<close>
 
 lemma "\<exists>r. xpos r = x"
-  by (tactic \<open>simp_tac (put_simpset HOL_basic_ss \<^context>
-    addsimprocs [Record.ex_sel_eq_simproc]) 1\<close>)
+  supply [[simproc add: Record.ex_sel_eq]]
+  apply (simp)
+  done
+
+subsection \<open>Simprocs for update and equality\<close>
+
+record alph1 =
+a::nat
+b::nat
+
+record alph2 = alph1 +
+c::nat
+d::nat
+
+record alph3 = alph2 + 
+  e::nat
+  f::nat
+
+text \<open>The simprocs that are activated by default are:
+\<^item> @{ML [source] Record.simproc}: field selection of (nested) record updates.
+\<^item> @{ML [source] Record.upd_simproc}: nested record updates.
+\<^item> @{ML [source] Record.eq_simproc}: (componentwise) equality of records.
+\<close>
+
+
+text \<open>By default record updates are not ordered by simplification.\<close>
+schematic_goal "r\<lparr>b := x, a:= y\<rparr> = ?X"
+  by simp
+
+text \<open>Normalisation towards an update ordering (string ordering of update function names) can
+be configured as follows.\<close>
+schematic_goal "r\<lparr>b := y, a := x\<rparr> = ?X"
+  supply [[record_sort_updates]]
+  by simp
+
+text \<open>Note the interplay between update ordering and record equality. Without update ordering
+the following equality is handled by @{ML [source] Record.eq_simproc}. Record equality is thus
+solved by componentwise comparison of all the fields of the records which can be expensive 
+in the presence of many fields.\<close>
+
+lemma "r\<lparr>f := x1, a:= x2\<rparr> = r\<lparr>a := x2, f:= x1\<rparr>"
+  by simp
+
+lemma "r\<lparr>f := x1, a:= x2\<rparr> = r\<lparr>a := x2, f:= x1\<rparr>"
+  supply [[simproc del: Record.eq]]
+  apply (simp?)
+  oops
+
+text \<open>With update ordering the equality is already established after update normalisation. There
+is no need for componentwise comparison.\<close>
+
+lemma "r\<lparr>f := x1, a:= x2\<rparr> = r\<lparr>a := x2, f:= x1\<rparr>"
+  supply [[record_sort_updates, simproc del: Record.eq]]
+  apply simp
+  done
+
+schematic_goal "r\<lparr>f := x1, e := x2, d:= x3, c:= x4, b:=x5, a:= x6\<rparr> = ?X"
+  supply [[record_sort_updates]]
+  by simp
+
+schematic_goal "r\<lparr>f := x1, e := x2, d:= x3, c:= x4, e:=x5, a:= x6\<rparr> = ?X"
+  supply [[record_sort_updates]]
+  by simp
+
+schematic_goal "r\<lparr>f := x1, e := x2, d:= x3, c:= x4, e:=x5, a:= x6\<rparr> = ?X"
+  by simp
 
 
 subsection \<open>A more complex record expression\<close>
@@ -324,6 +389,24 @@
   bar520 :: nat
   bar521 :: "nat \<times> nat"
 
-declare [[record_codegen = true]]
+
+setup \<open>
+let
+ val N = 300
+in
+  Record.add_record {overloaded=false} ([], \<^binding>\<open>large_record\<close>) NONE 
+    (map (fn i => (Binding.make ("fld_" ^ string_of_int i, \<^here>), @{typ nat}, Mixfix.NoSyn)) 
+      (1 upto N))
+end
+\<close>
+
+declare [[record_codegen]]
+
+schematic_goal \<open>fld_1 (r\<lparr>fld_300 := x300, fld_20 := x20, fld_200 := x200\<rparr>) = ?X\<close>
+  by simp
+
+schematic_goal \<open>r\<lparr>fld_300 := x300, fld_20 := x20, fld_200 := x200\<rparr> = ?X\<close>
+  supply [[record_sort_updates]]
+  by simp
 
 end
diff -r c2fd8b88d262 -r e07d873c18a4 src/HOL/Library/conditional_parametricity.ML
--- a/src/HOL/Library/conditional_parametricity.ML	Fri Sep 02 13:41:55 2022 +0200
+++ b/src/HOL/Library/conditional_parametricity.ML	Wed Sep 07 08:58:27 2022 +0200
@@ -110,8 +110,7 @@
 (* Tactics  *)
 (* helper tactics for printing *)
 fun error_tac ctxt msg st =
-  (error(msg ^ "\n" ^ Pretty.string_of (Pretty.chunks (Goal_Display.pretty_goals ctxt st)));
-  Seq.single st);
+  (error (msg ^ "\n" ^ Goal_Display.string_of_goal ctxt st); Seq.single st);
 
 fun error_tac' ctxt msg = SELECT_GOAL (error_tac ctxt msg);
 
diff -r c2fd8b88d262 -r e07d873c18a4 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Sep 02 13:41:55 2022 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Wed Sep 07 08:58:27 2022 +0200
@@ -245,12 +245,14 @@
     (if keep_chained then is_fact_chained else K false))
 
 val max_fact_instances = 10 (* FUDGE *)
+val max_schematics = 20 (* FUDGE *)
 
 fun repair_monomorph_context max_iters best_max_iters max_new_instances best_max_new_instances =
   Config.put Monomorph.max_rounds (max_iters |> the_default best_max_iters)
   #> Config.put Monomorph.max_new_instances
        (max_new_instances |> the_default best_max_new_instances)
   #> Config.put Monomorph.max_thm_instances max_fact_instances
+  #> Config.put Monomorph.max_schematics max_schematics
 
 fun supported_provers ctxt =
   let
diff -r c2fd8b88d262 -r e07d873c18a4 src/HOL/Tools/monomorph.ML
--- a/src/HOL/Tools/monomorph.ML	Fri Sep 02 13:41:55 2022 +0200
+++ b/src/HOL/Tools/monomorph.ML	Wed Sep 07 08:58:27 2022 +0200
@@ -36,6 +36,7 @@
   val max_rounds: int Config.T
   val max_new_instances: int Config.T
   val max_thm_instances: int Config.T
+  val max_schematics: int Config.T
   val max_new_const_instances_per_round: int Config.T
   val max_duplicated_instances: int Config.T
 
@@ -72,6 +73,9 @@
 val max_thm_instances =
   Attrib.setup_config_int \<^binding>\<open>monomorph_max_thm_instances\<close> (K 20)
 
+val max_schematics =
+  Attrib.setup_config_int \<^binding>\<open>monomorph_max_schematics\<close> (K 1000)
+
 val max_new_const_instances_per_round =
   Attrib.setup_config_int \<^binding>\<open>monomorph_max_new_const_instances_per_round\<close> (K 5)
 
@@ -177,8 +181,8 @@
       | add _ = I
   in Term.fold_aterms add (Thm.prop_of thm) end
 
-fun add_insts max_instances max_duplicated_instances max_thm_insts ctxt round used_grounds
-    new_grounds id thm tvars schematics cx =
+fun add_insts max_instances max_duplicated_instances max_thm_insts max_schematics ctxt round
+    used_grounds new_grounds id thm tvars schematics cx =
   let
     exception ENOUGH of
       typ list Symtab.table * (int * int * ((int * (sort * typ) Vartab.table) * thm) list Inttab.table)
@@ -242,22 +246,24 @@
        instance is the usage of at least one ground from the new_grounds
        table. The approach used here is to match all schematics of the theorem
        with all relevant grounds. *)
-    for_schematics false schematics Vartab.empty cx
+    if length schematics > max_schematics then cx
+    else for_schematics false schematics Vartab.empty cx
     handle ENOUGH cx' => cx'
   end
 
 fun is_new round initial_round = (round = initial_round)
 fun is_active round initial_round = (round > initial_round)
 
-fun find_instances max_instances max_duplicated_instances max_thm_insts max_new_grounds thm_infos
-    ctxt round (known_grounds, new_grounds0, insts) =
+fun find_instances max_instances max_duplicated_instances max_thm_insts max_schematics
+    max_new_grounds thm_infos ctxt round (known_grounds, new_grounds0, insts) =
   let
     val new_grounds =
       Symtab.map (fn _ => fn grounds =>
         if length grounds <= max_new_grounds then grounds
         else take max_new_grounds (sort Term_Ord.typ_ord grounds)) new_grounds0
 
-    val add_new = add_insts max_instances max_duplicated_instances max_thm_insts ctxt round
+    val add_new = add_insts max_instances max_duplicated_instances max_thm_insts max_schematics
+      ctxt round
     fun consider_all pred f (cx as (_, (hits, misses, _))) =
       if hits >= max_instances orelse misses >= max_duplicated_instances then
         cx
@@ -279,7 +285,7 @@
   let fun add (n, T) = Symtab.map_entry n (insert (op =) T)
   in Term.fold_aterms (fn Const c => add c | _ => I) (Thm.prop_of thm) end
 
-fun collect_instances ctxt max_thm_insts max_new_grounds thm_infos consts =
+fun collect_instances ctxt max_thm_insts max_schematics max_new_grounds thm_infos consts =
   let
     val known_grounds = fold_grounds add_ground_types thm_infos consts
     val empty_grounds = clear_grounds known_grounds
@@ -288,7 +294,8 @@
     val max_duplicated_instances = Config.get ctxt max_duplicated_instances
     val (_, _, (_, _, insts)) =
       limit_rounds ctxt (find_instances max_instances max_duplicated_instances max_thm_insts
-      max_new_grounds thm_infos) (empty_grounds, known_grounds, (0, 0, Inttab.empty))
+          max_schematics max_new_grounds thm_infos)
+        (empty_grounds, known_grounds, (0, 0, Inttab.empty))
   in
     insts
   end
@@ -313,11 +320,14 @@
 fun monomorph schematic_consts_of ctxt rthms =
   let
     val max_thm_insts = Config.get ctxt max_thm_instances
+    val max_schematics = Config.get ctxt max_schematics
     val max_new_grounds = Config.get ctxt max_new_const_instances_per_round
     val (thm_infos, consts) = prepare schematic_consts_of rthms
     val insts =
-      if Symtab.is_empty consts then Inttab.empty
-      else collect_instances ctxt max_thm_insts max_new_grounds thm_infos consts
+      if Symtab.is_empty consts then
+        Inttab.empty
+      else
+        collect_instances ctxt max_thm_insts max_schematics max_new_grounds thm_infos consts
   in map (instantiated_thms max_thm_insts insts) thm_infos end
 
 end
diff -r c2fd8b88d262 -r e07d873c18a4 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Fri Sep 02 13:41:55 2022 +0200
+++ b/src/HOL/Tools/record.ML	Wed Sep 07 08:58:27 2022 +0200
@@ -2,6 +2,7 @@
     Author:     Wolfgang Naraschewski, TU Muenchen
     Author:     Markus Wenzel, TU Muenchen
     Author:     Norbert Schirmer, TU Muenchen
+    Author:     Norbert Schirmer, Apple, 2022
     Author:     Thomas Sewell, NICTA
 
 Extensible records with structural subtyping.
@@ -50,6 +51,7 @@
   val string_of_record: Proof.context -> string -> string
 
   val codegen: bool Config.T
+  val sort_updates: bool Config.T
   val updateN: string
   val ext_typeN: string
   val extN: string
@@ -196,6 +198,7 @@
 val updacc_cong_from_eq = @{thm iso_tuple_update_accessor_cong_from_eq};
 
 val codegen = Attrib.setup_config_bool \<^binding>\<open>record_codegen\<close> (K true);
+val sort_updates = Attrib.setup_config_bool \<^binding>\<open>record_sort_updates\<close> (K false);
 
 
 (** name components **)
@@ -984,9 +987,8 @@
     val dest = if comp then @{thm o_eq_dest_lhs} else @{thm o_eq_dest};
   in Drule.export_without_context (othm RS dest) end;
 
-fun get_updupd_simps ctxt term defset =
+fun gen_get_updupd_simps ctxt upd_funs defset =
   let
-    val upd_funs = get_upd_funs term;
     val cname = fst o dest_Const;
     fun getswap u u' = get_updupd_simp ctxt defset u u' (cname u = cname u');
     fun build_swaps_to_eq _ [] swaps = swaps
@@ -1007,7 +1009,9 @@
           else swaps_needed us (u :: prev) (Symtab.insert (K true) (cname u, ()) seen) swaps;
   in swaps_needed upd_funs [] Symtab.empty Symreltab.empty end;
 
-fun prove_unfold_defs thy ex_simps ex_simprs prop =
+fun get_updupd_simps ctxt term defset = gen_get_updupd_simps ctxt (get_upd_funs term) defset;
+
+fun prove_unfold_defs thy upd_funs ex_simps ex_simprs prop =
   let
     val ctxt = Proof_Context.init_global thy;
 
@@ -1015,7 +1019,10 @@
     val prop' = Envir.beta_eta_contract prop;
     val (lhs, _) = Logic.dest_equals (Logic.strip_assums_concl prop');
     val (_, args) = strip_comb lhs;
-    val simps = (if length args = 1 then get_accupd_simps else get_updupd_simps) ctxt lhs defset;
+    val simps =
+      if null upd_funs then
+        (if length args = 1 then get_accupd_simps else get_updupd_simps) ctxt lhs defset
+      else gen_get_updupd_simps ctxt upd_funs defset
   in
     Goal.prove ctxt [] [] prop'
       (fn {context = ctxt', ...} =>
@@ -1053,8 +1060,7 @@
   - If X is a more-selector we have to make sure that S is not in the updated
     subrecord.
 *)
-val simproc =
-  Simplifier.make_simproc \<^context> "record"
+val  _ = Theory.setup (Named_Target.theory_map (Simplifier.define_simproc \<^binding>\<open>select_update\<close>
    {lhss = [\<^term>\<open>x::'a::{}\<close>],
     proc = fn _ => fn ctxt => fn ct =>
       let
@@ -1102,13 +1108,17 @@
                 (case mk_eq_terms (upd $ k $ r) of
                   SOME (trm, trm', vars) =>
                     SOME
-                      (prove_unfold_defs thy [] []
+                      (prove_unfold_defs thy [] [] []
                         (Logic.list_all (vars, Logic.mk_equals (sel $ trm, trm'))))
                 | NONE => NONE)
               end
             else NONE
         | _ => NONE)
-      end};
+      end}));
+
+val simproc_name =
+  Simplifier.check_simproc (Context.the_local_context ()) ("select_update", Position.none);
+val simproc = Simplifier.the_simproc (Context.the_local_context ()) simproc_name;
 
 fun get_upd_acc_cong_thm upd acc thy ss =
   let
@@ -1126,6 +1136,24 @@
         TRY (resolve_tac ctxt' [updacc_cong_idI] 1))
   end;
 
+fun sorted ord [] = true
+  | sorted ord [x] = true
+  | sorted ord (x::y::xs) =
+      (case ord (x, y) of
+         LESS => sorted ord (y::xs)
+       | EQUAL => sorted ord (y::xs)
+       | GREATER => false)
+
+fun insert_unique ord x [] = [x]
+  | insert_unique ord x (y::ys) =
+      (case ord (x, y) of
+         LESS => (x::y::ys)
+       | EQUAL => (x::ys)
+       | GREATER => y :: insert_unique ord x ys)
+
+fun insert_unique_hd ord (x::xs) = x :: insert_unique ord x xs
+  | insert_unique_hd ord xs = xs
+
 
 (* upd_simproc *)
 
@@ -1137,8 +1165,7 @@
   In both cases "more" updates complicate matters: for this reason
   we omit considering further updates if doing so would introduce
   both a more update and an update to a field within it.*)
-val upd_simproc =
-  Simplifier.make_simproc \<^context> "record_upd"
+val  _ = Theory.setup (Named_Target.theory_map (Simplifier.define_simproc \<^binding>\<open>update\<close>
    {lhss = [\<^term>\<open>x::'a::{}\<close>],
     proc = fn _ => fn ctxt => fn ct =>
       let
@@ -1169,6 +1196,13 @@
           | getupdseq term _ _ = ([], term, HOLogic.unitT);
 
         val (upds, base, baseT) = getupdseq t 0 ~1;
+        val orig_upds = map_index (fn (i, (x, y, z)) => (x, y, z, i)) upds
+        val upd_ord = rev_order o fast_string_ord o apply2 #2
+        val (upds, commuted) =
+          if not (null orig_upds) andalso Config.get ctxt sort_updates andalso not (sorted upd_ord orig_upds) then
+             (sort upd_ord orig_upds, true)
+          else
+             (orig_upds, false)
 
         fun is_upd_noop s (Abs (n, T, Const (s', T') $ tm')) tm =
               if s = s' andalso null (loose_bnos tm')
@@ -1193,7 +1227,7 @@
           | add_upd f fs = (f :: fs);
 
         (*mk_updterm returns
-          (orig-term-skeleton, simplified-skeleton,
+          (orig-term-skeleton-update list , simplified-skeleton,
             variables, duplicate-updates, simp-flag, noop-simps)
 
           where duplicate-updates is a table used to pass upward
@@ -1201,9 +1235,9 @@
           into an update above them, simp-flag indicates whether
           any simplification was achieved, and noop-simps are
           used for eliminating case (2) defined above*)
-        fun mk_updterm ((upd as Const (u, T), s, f) :: upds) above term =
+        fun mk_updterm ((upd as Const (u, T), s, f, i) :: upds) above term =
               let
-                val (lhs, rhs, vars, dups, simp, noops) =
+                val (lhs_upds, rhs, vars, dups, simp, noops) =
                   mk_updterm upds (Symtab.update (u, ()) above) term;
                 val (fvar, skelf) =
                   K_skeleton (Long_Name.base_name s) (domain_type T) (Bound (length vars)) f;
@@ -1213,35 +1247,46 @@
                   Const (\<^const_name>\<open>Fun.comp\<close>, funT --> funT --> funT) $ f $ f';
               in
                 if isnoop then
-                  (upd $ skelf' $ lhs, rhs, vars,
+                  ((upd $ skelf', i)::lhs_upds, rhs, vars,
                     Symtab.update (u, []) dups, true,
                     if Symtab.defined noops u then noops
                     else Symtab.update (u, get_noop_simps upd skelf') noops)
                 else if Symtab.defined above u then
-                  (upd $ skelf $ lhs, rhs, fvar :: vars,
+                  ((upd $ skelf, i)::lhs_upds, rhs, fvar :: vars,
                     Symtab.map_default (u, []) (add_upd skelf) dups,
                     true, noops)
                 else
                   (case Symtab.lookup dups u of
                     SOME fs =>
-                     (upd $ skelf $ lhs,
+                     ((upd $ skelf, i)::lhs_upds,
                       upd $ foldr1 mk_comp_local (add_upd skelf fs) $ rhs,
                       fvar :: vars, dups, true, noops)
-                  | NONE => (upd $ skelf $ lhs, upd $ skelf $ rhs, fvar :: vars, dups, simp, noops))
+                  | NONE => ((upd $ skelf, i)::lhs_upds, upd $ skelf $ rhs, fvar :: vars, dups, simp, noops))
               end
           | mk_updterm [] _ _ =
-              (Bound 0, Bound 0, [("r", baseT)], Symtab.empty, false, Symtab.empty)
-          | mk_updterm us _ _ = raise TERM ("mk_updterm match", map (fn (x, _, _) => x) us);
-
-        val (lhs, rhs, vars, _, simp, noops) = mk_updterm upds Symtab.empty base;
+              ([], Bound 0, [("r", baseT)], Symtab.empty, false, Symtab.empty)
+          | mk_updterm us _ _ = raise TERM ("mk_updterm match", map (fn (x, _, _, _) => x) us);
+
+        val (lhs_upds, rhs, vars, _, simp, noops) = mk_updterm upds Symtab.empty base;
+        val orig_order_lhs_upds = lhs_upds |> sort (rev_order o int_ord o apply2 snd)
+        val lhs = Bound 0 |> fold (fn (upd, _) => fn s => upd $ s) orig_order_lhs_upds
+        (* Note that the simplifier works bottom up. So all nested updates are already
+           normalised, e.g. sorted. 'commuted' thus means that the outermost update has to be
+           inserted at its place inside the sorted nested updates. The necessary swaps can be
+           expressed via 'upd_funs' by replicating the outer update at the designated position: *)
+        val upd_funs = (if commuted then insert_unique_hd upd_ord orig_upds else orig_upds) |> map #1
         val noops' = maps snd (Symtab.dest noops);
       in
-        if simp then
+        if simp orelse commuted then
           SOME
-            (prove_unfold_defs thy noops' [simproc]
+            (prove_unfold_defs thy upd_funs noops' [simproc]
               (Logic.list_all (vars, Logic.mk_equals (lhs, rhs))))
         else NONE
-      end};
+      end}));
+
+val upd_simproc_name =
+  Simplifier.check_simproc (Context.the_local_context ()) ("update", Position.none);
+val upd_simproc = Simplifier.the_simproc (Context.the_local_context ()) upd_simproc_name;
 
 end;
 
@@ -1260,8 +1305,8 @@
              eq_simproc          split_simp_tac
  Complexity: #components * #updates     #updates
 *)
-val eq_simproc =
-  Simplifier.make_simproc \<^context> "record_eq"
+
+val  _ = Theory.setup (Named_Target.theory_map (Simplifier.define_simproc \<^binding>\<open>eq\<close>
    {lhss = [\<^term>\<open>r = s\<close>],
     proc = fn _ => fn ctxt => fn ct =>
       (case Thm.term_of ct of
@@ -1272,8 +1317,10 @@
               (case get_equalities (Proof_Context.theory_of ctxt) name of
                 NONE => NONE
               | SOME thm => SOME (thm RS @{thm Eq_TrueI})))
-      | _ => NONE)};
-
+      | _ => NONE)}));
+
+val eq_simproc_name = Simplifier.check_simproc (Context.the_local_context ()) ("eq", Position.none);
+val eq_simproc = Simplifier.the_simproc (Context.the_local_context ()) eq_simproc_name;
 
 (* split_simproc *)
 
@@ -1311,8 +1358,7 @@
           else NONE
       | _ => NONE)};
 
-val ex_sel_eq_simproc =
-  Simplifier.make_simproc \<^context> "ex_sel_eq"
+val  _ = Theory.setup (Named_Target.theory_map (Simplifier.define_simproc \<^binding>\<open>ex_sel_eq\<close>
    {lhss = [\<^term>\<open>Ex t\<close>],
     proc = fn _ => fn ctxt => fn ct =>
       let
@@ -1350,7 +1396,12 @@
                     addsimps @{thms simp_thms} addsimprocs [split_simproc (K ~1)]) 1))
             end handle TERM _ => NONE)
         | _ => NONE)
-      end};
+      end}));
+
+val ex_sel_eq_simproc_name =
+  Simplifier.check_simproc (Context.the_local_context ()) ("ex_sel_eq", Position.none);
+val ex_sel_eq_simproc = Simplifier.the_simproc (Context.the_local_context ()) ex_sel_eq_simproc_name;
+val _ = Theory.setup (map_theory_simpset (fn ctxt => ctxt delsimprocs [ex_sel_eq_simproc]));
 
 
 (* split_simp_tac *)
@@ -1431,11 +1482,6 @@
     else no_tac
   end);
 
-val _ =
-  Theory.setup
-    (map_theory_simpset (fn ctxt => ctxt addsimprocs [simproc, upd_simproc, eq_simproc]));
-
-
 (* wrapper *)
 
 val split_name = "record_split_tac";
diff -r c2fd8b88d262 -r e07d873c18a4 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Fri Sep 02 13:41:55 2022 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Sep 07 08:58:27 2022 +0200
@@ -1147,13 +1147,13 @@
 
 fun schematic_goal state =
   let val (_, {statement = (_, _, prop), ...}) = find_goal state
-  in Goal.is_schematic prop end;
+  in Term.is_schematic prop end;
 
 fun is_relevant state =
   (case try find_goal state of
     NONE => true
   | SOME (_, {statement = (_, _, prop), goal, ...}) =>
-      Goal.is_schematic prop orelse not (Logic.protect prop aconv Thm.concl_of goal));
+      Term.is_schematic prop orelse not (Logic.protect prop aconv Thm.concl_of goal));
 
 
 (* terminal proof steps *)
diff -r c2fd8b88d262 -r e07d873c18a4 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Fri Sep 02 13:41:55 2022 +0200
+++ b/src/Pure/PIDE/resources.ML	Wed Sep 07 08:58:27 2022 +0200
@@ -256,9 +256,11 @@
     SOME qualifier => qualifier
   | NONE => Long_Name.qualifier theory);
 
+fun literal_theory theory =
+  Long_Name.is_qualified theory orelse is_some (global_theory theory);
+
 fun theory_name qualifier theory =
-  if Long_Name.is_qualified theory orelse is_some (global_theory theory)
-  then theory
+  if literal_theory theory then theory
   else Long_Name.qualify qualifier theory;
 
 fun theory_bibtex_entries theory =
@@ -284,15 +286,21 @@
 fun import_name qualifier dir s =
   let
     val theory = theory_name qualifier (Thy_Header.import_name s);
-    fun theory_node () =
-      make_theory_node (File.full_path dir (thy_path (Path.expand (Path.explode s)))) theory;
+    fun theory_node path = make_theory_node path theory;
+    val literal_import = literal_theory theory andalso qualifier <> theory_qualifier theory;
+    val _ =
+      if literal_import andalso not (Thy_Header.is_base_name s) then
+        error ("Bad import of theory from other session via file-path: " ^ quote s)
+      else ();
   in
-    if not (Thy_Header.is_base_name s) then theory_node ()
-    else if loaded_theory theory then loaded_theory_node theory
+    if loaded_theory theory then loaded_theory_node theory
     else
       (case find_theory_file theory of
-        SOME node_name => make_theory_node node_name theory
-      | NONE => if Long_Name.is_qualified s then loaded_theory_node theory else theory_node ())
+        SOME node_name => theory_node node_name
+      | NONE =>
+          if Thy_Header.is_base_name s andalso Long_Name.is_qualified s
+          then loaded_theory_node theory
+          else theory_node (File.full_path dir (thy_path (Path.expand (Path.explode s)))))
   end;
 
 fun check_file dir file = File.check_file (File.full_path dir file);
diff -r c2fd8b88d262 -r e07d873c18a4 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Fri Sep 02 13:41:55 2022 +0200
+++ b/src/Pure/PIDE/resources.scala	Wed Sep 07 08:58:27 2022 +0200
@@ -150,8 +150,11 @@
   def global_theory(theory: String): Boolean =
     sessions_structure.global_theories.isDefinedAt(theory)
 
+  def literal_theory(theory: String): Boolean =
+    Long_Name.is_qualified(theory) || global_theory(theory)
+
   def theory_name(qualifier: String, theory: String): String =
-    if (Long_Name.is_qualified(theory) || global_theory(theory)) theory
+    if (literal_theory(theory)) theory
     else Long_Name.qualify(qualifier, theory)
 
   def find_theory_node(theory: String): Option[Document.Node.Name] = {
@@ -168,14 +171,18 @@
 
   def import_name(qualifier: String, dir: String, s: String): Document.Node.Name = {
     val theory = theory_name(qualifier, Thy_Header.import_name(s))
-    def theory_node = file_node(Path.explode(s).thy, dir = dir, theory = theory)
-
-    if (!Thy_Header.is_base_name(s)) theory_node
-    else if (session_base.loaded_theory(theory)) loaded_theory_node(theory)
+    val literal_import =
+      literal_theory(theory) && qualifier != sessions_structure.theory_qualifier(theory)
+    if (literal_import && !Thy_Header.is_base_name(s)) {
+      error("Bad import of theory from other session via file-path: " + quote(s))
+    }
+    if (session_base.loaded_theory(theory)) loaded_theory_node(theory)
     else {
       find_theory_node(theory) match {
         case Some(node_name) => node_name
-        case None => if (Long_Name.is_qualified(s)) loaded_theory_node(theory) else theory_node
+        case None =>
+          if (Thy_Header.is_base_name(s) && literal_theory(s)) loaded_theory_node(theory)
+          else file_node(Path.explode(s).thy, dir = dir, theory = theory)
       }
     }
   }
diff -r c2fd8b88d262 -r e07d873c18a4 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Fri Sep 02 13:41:55 2022 +0200
+++ b/src/Pure/PIDE/session.scala	Wed Sep 07 08:58:27 2022 +0200
@@ -65,7 +65,6 @@
   case object Caret_Focus
   case class Raw_Edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
   case class Dialog_Result(id: Document_ID.Generic, serial: Long, result: String)
-  case class Build_Theories(id: String, master_dir: Path, theories: List[(Options, List[Path])])
   case class Commands_Changed(
     assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command])
 
diff -r c2fd8b88d262 -r e07d873c18a4 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Sep 02 13:41:55 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Wed Sep 07 08:58:27 2022 +0200
@@ -193,8 +193,9 @@
 
             val imported_files = if (inlined_files) dependencies.imported_files else Nil
 
-            if (list_files)
+            if (list_files) {
               progress.echo(cat_lines(session_files.map(_.implode).sorted.map("  " + _)))
+            }
 
             if (check_keywords.nonEmpty) {
               Check_Keywords.check_keywords(
@@ -207,8 +208,9 @@
 
               def node(name: Document.Node.Name): Graph_Display.Node = {
                 val qualifier = sessions_structure.theory_qualifier(name)
-                if (qualifier == info.name)
+                if (qualifier == info.name) {
                   Graph_Display.Node(name.theory_base_name, "theory." + name.theory)
+                }
                 else session_node(qualifier)
               }
 
@@ -590,9 +592,10 @@
         for { (_, thys) <- entry.theories; ((thy, pos), global) <- thys if global }
         yield {
           val thy_name = Path.explode(thy).file_name
-          if (Long_Name.is_qualified(thy_name))
+          if (Long_Name.is_qualified(thy_name)) {
             error("Bad qualified name for global theory " +
               quote(thy_name) + Position.here(pos))
+          }
           else thy_name
         }
 
@@ -664,9 +667,10 @@
         edges: Info => Iterable[String]
       ) : Graph[String, Info] = {
         def add_edge(pos: Position.T, name: String, g: Graph[String, Info], parent: String) = {
-          if (!g.defined(parent))
+          if (!g.defined(parent)) {
             error("Bad " + kind + " session " + quote(parent) + " for " +
               quote(name) + Position.here(pos))
+          }
 
           try { g.add_edge_acyclic(parent, name) }
           catch {
@@ -685,9 +689,10 @@
       val info_graph =
         infos.foldLeft(Graph.string[Info]) {
           case (graph, info) =>
-            if (graph.defined(info.name))
+            if (graph.defined(info.name)) {
               error("Duplicate session " + quote(info.name) + Position.here(info.pos) +
                 Position.here(graph.get_node(info.name).pos))
+            }
             else graph.new_node(info.name, info)
         }
       val build_graph = add_edges(info_graph, "parent", _.parent)
@@ -784,8 +789,9 @@
 
     def check_sessions(names: List[String]): Unit = {
       val bad_sessions = SortedSet(names.filterNot(defined): _*).toList
-      if (bad_sessions.nonEmpty)
+      if (bad_sessions.nonEmpty) {
         error("Undefined session(s): " + commas_quote(bad_sessions))
+      }
     }
 
     def check_sessions(sel: Selection): Unit =
diff -r c2fd8b88d262 -r e07d873c18a4 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Fri Sep 02 13:41:55 2022 +0200
+++ b/src/Pure/goal.ML	Wed Sep 07 08:58:27 2022 +0200
@@ -25,7 +25,6 @@
   val skip_proofs_enabled: unit -> bool
   val future_result: Proof.context -> thm future -> term -> thm
   val prove_internal: Proof.context -> cterm list -> cterm -> (thm list -> tactic) -> thm
-  val is_schematic: term -> bool
   val prove_common: Proof.context -> int option -> string list -> term list -> term list ->
     ({prems: thm list, context: Proof.context} -> tactic) -> thm list
   val prove_future: Proof.context -> string list -> term list -> term ->
@@ -81,8 +80,7 @@
 *)
 fun check_finished ctxt th =
   if Thm.no_prems th then th
-  else
-    raise THM ("Proof failed.\n" ^ Pretty.string_of (Goal_Display.pretty_goal ctxt th), 0, [th]);
+  else raise THM ("Proof failed.\n" ^ Goal_Display.string_of_goal ctxt th, 0, [th]);
 
 fun finish ctxt = check_finished ctxt #> conclude;
 
@@ -162,15 +160,11 @@
 
 (* prove variations *)
 
-fun is_schematic t =
-  Term.exists_subterm Term.is_Var t orelse
-  Term.exists_type (Term.exists_subtype Term.is_TVar) t;
-
 fun prove_common ctxt fork_pri xs asms props tac =
   let
     val thy = Proof_Context.theory_of ctxt;
 
-    val schematic = exists is_schematic props;
+    val schematic = exists Term.is_schematic props;
     val immediate = is_none fork_pri;
     val future = Future.proofs_enabled 1 andalso not (Proofterm.proofs_enabled ());
     val skip = not immediate andalso not schematic andalso future andalso skip_proofs_enabled ();
diff -r c2fd8b88d262 -r e07d873c18a4 src/Pure/tactical.ML
--- a/src/Pure/tactical.ML	Fri Sep 02 13:41:55 2022 +0200
+++ b/src/Pure/tactical.ML	Wed Sep 07 08:58:27 2022 +0200
@@ -176,8 +176,7 @@
 
 (*Print the current proof state and pass it on.*)
 fun print_tac ctxt msg st =
- (tracing (msg ^ "\n" ^ Pretty.string_of (Pretty.chunks (Goal_Display.pretty_goals ctxt st)));
-  Seq.single st);
+  (tracing (msg ^ "\n" ^ Goal_Display.string_of_goal ctxt st); Seq.single st);
 
 
 (*Deterministic REPEAT: only retains the first outcome;
diff -r c2fd8b88d262 -r e07d873c18a4 src/Pure/term.ML
--- a/src/Pure/term.ML	Fri Sep 02 13:41:55 2022 +0200
+++ b/src/Pure/term.ML	Wed Sep 07 08:58:27 2022 +0200
@@ -114,6 +114,7 @@
   val exists_type: (typ -> bool) -> term -> bool
   val exists_subterm: (term -> bool) -> term -> bool
   val exists_Const: (string * typ -> bool) -> term -> bool
+  val is_schematic: term -> bool
 end;
 
 signature TERM =
@@ -950,6 +951,10 @@
 
 fun exists_Const P = exists_subterm (fn Const c => P c | _ => false);
 
+fun is_schematic t =
+  exists_subterm is_Var t orelse
+  (exists_type o exists_subtype) is_TVar t;
+
 
 (* contraction *)
 
diff -r c2fd8b88d262 -r e07d873c18a4 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Fri Sep 02 13:41:55 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Wed Sep 07 08:58:27 2022 +0200
@@ -30,19 +30,19 @@
   override def flush(): Unit = flush_edits()
   def purge(): Unit = flush_edits(purge = true)
 
-  private val delay1_flush =
+  private val delay_input: Delay =
     Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) { flush() }
 
-  private val delay2_flush =
+  private val delay_generated_input: Delay =
     Delay.first(PIDE.options.seconds("editor_generated_input_delay"), gui = true) { flush() }
 
-  def invoke(): Unit = delay1_flush.invoke()
-  def invoke_generated(): Unit = { delay1_flush.invoke(); delay2_flush.invoke() }
+  def invoke(): Unit = delay_input.invoke()
+  def invoke_generated(): Unit = { delay_input.invoke(); delay_generated_input.invoke() }
 
   def shutdown(): Unit =
     GUI_Thread.require {
-      delay1_flush.revoke()
-      delay2_flush.revoke()
+      delay_input.revoke()
+      delay_generated_input.revoke()
       Document_Model.flush_edits(hidden = false, purge = false)
     }