merged
authorwenzelm
Fri, 17 Jan 2025 21:30:08 +0100
changeset 81867 f0ae2acbefd5
parent 81822 e7be7c4b871c (diff)
parent 81866 fa0bafdc0fc6 (current diff)
child 81868 d832c4a676e1
merged
src/Pure/System/isabelle_system.scala
--- a/NEWS	Fri Jan 17 20:30:01 2025 +0100
+++ b/NEWS	Fri Jan 17 21:30:08 2025 +0100
@@ -235,6 +235,9 @@
 types by target-language operations; this is also used by
 HOL-Library.Code_Target_Numeral.
 
+* Theory HOL-Library.Code_Bit_Shifts_for_Arithmetic rewrites certain
+arithmetic operations on numerals to bit shifts.
+
 * Sledgehammer:
   - Update of bundled provers:
       . E 3.1 -- with patch on Windows/Cygwin for proper interrupts
--- a/etc/options	Fri Jan 17 20:30:01 2025 +0100
+++ b/etc/options	Fri Jan 17 21:30:08 2025 +0100
@@ -234,6 +234,9 @@
 option build_schedule_inactive_delay : real = 300.0
   -- "delay removing inactive hosts"
 
+option build_schedule_history : int = 150
+  -- "length of history relevant for scheduling (in days)"
+
 
 section "Build Manager"
 
--- a/src/HOL/Cardinals/Wellorder_Constructions.thy	Fri Jan 17 20:30:01 2025 +0100
+++ b/src/HOL/Cardinals/Wellorder_Constructions.thy	Fri Jan 17 21:30:08 2025 +0100
@@ -322,7 +322,7 @@
   shows "P a"
   by (induct rule: well_order_induct) (rule assms, simp add: underS_def)
 
-lemma suc_underS:
+lemma suc_underS':
   assumes B: "B \<subseteq> Field r" and A: "AboveS B \<noteq> {}" and b: "b \<in> B"
   shows "b \<in> underS (suc B)"
   using suc_AboveS[OF B A] b unfolding underS_def AboveS_def by auto
--- a/src/HOL/Codegenerator_Test/Code_Test_GHC.thy	Fri Jan 17 20:30:01 2025 +0100
+++ b/src/HOL/Codegenerator_Test/Code_Test_GHC.thy	Fri Jan 17 21:30:08 2025 +0100
@@ -26,163 +26,4 @@
 
 test_code "stake 10 (cycle ''ab'') = ''ababababab''" in GHC
 
-text \<open>Test cases for bit operations on target language numerals\<close>
-
-unbundle bit_operations_syntax
-
-lemma \<open>bit (473514 :: integer) 5\<close>
-  by normalization
-
-test_code \<open>bit (473514 :: integer) 5\<close> in GHC
-
-lemma \<open>bit (- 805167 :: integer) 7\<close>
-  by normalization
-
-test_code \<open>bit (- 805167 :: integer) 7\<close> in GHC
-
-lemma \<open>473514 AND (767063 :: integer) = 208898\<close>
-  by normalization
-
-test_code \<open>473514 AND (767063 :: integer) = 208898\<close> in GHC
-
-lemma \<open>- 805167 AND (767063 :: integer) = 242769\<close>
-  by normalization
-
-test_code \<open>- 805167 AND (767063 :: integer) = 242769\<close> in GHC
-
-lemma \<open>473514 AND (- 314527 :: integer) = 209184\<close>
-  by normalization
-
-test_code \<open>473514 AND (- 314527 :: integer) = 209184\<close> in GHC
-
-lemma \<open>- 805167 AND (- 314527 :: integer) = - 839103\<close>
-  by normalization
-
-test_code \<open>- 805167 AND (- 314527 :: integer) = - 839103\<close> in GHC
-
-lemma \<open>473514 OR (767063 :: integer) = 1031679\<close>
-  by normalization
-
-test_code \<open>473514 OR (767063 :: integer) = 1031679\<close> in GHC
-
-lemma \<open>- 805167 OR (767063 :: integer) = - 280873\<close>
-  by normalization
-
-test_code \<open>- 805167 OR (767063 :: integer) = - 280873\<close> in GHC
-
-lemma \<open>473514 OR (- 314527 :: integer) = - 50197\<close>
-  by normalization
-
-test_code \<open>473514 OR (- 314527 :: integer) = - 50197\<close> in GHC
-
-lemma \<open>- 805167 OR (- 314527 :: integer) = - 280591\<close>
-  by normalization
-
-test_code \<open>- 805167 OR (- 314527 :: integer) = - 280591\<close> in GHC
-
-lemma \<open>473514 XOR (767063 :: integer) = 822781\<close>
-  by normalization
-
-test_code \<open>473514 XOR (767063 :: integer) = 822781\<close> in GHC
-
-lemma \<open>- 805167 XOR (767063 :: integer) = - 523642\<close>
-  by normalization
-
-test_code \<open>- 805167 XOR (767063 :: integer) = - 523642\<close> in GHC
-
-lemma \<open>473514 XOR (- 314527 :: integer) = - 259381\<close>
-  by normalization
-
-test_code \<open>473514 XOR (- 314527 :: integer) = - 259381\<close> in GHC
-
-lemma \<open>- 805167 XOR (- 314527 :: integer) = 558512\<close>
-  by normalization
-
-test_code \<open>- 805167 XOR (- 314527 :: integer) = 558512\<close> in GHC
-
-lemma \<open>NOT (473513 :: integer) = - 473514\<close>
-  by normalization
-
-test_code \<open>NOT (473513 :: integer) = - 473514\<close> in GHC
-
-lemma \<open>NOT (- 805167 :: integer) = 805166\<close>
-  by normalization
-
-test_code \<open>NOT (- 805167 :: integer) = 805166\<close> in GHC
-
-lemma \<open>(mask 39 :: integer) = 549755813887\<close>
-  by normalization
-
-test_code \<open>(mask 39 :: integer) = 549755813887\<close> in GHC
-
-lemma \<open>set_bit 15 (473514 :: integer) = 506282\<close>
-  by normalization
-
-test_code \<open>set_bit 15 (473514 :: integer) = 506282\<close> in GHC
-
-lemma \<open>set_bit 11 (- 805167 :: integer) = - 803119\<close>
-  by normalization
-
-test_code \<open>set_bit 11 (- 805167 :: integer) = - 803119\<close> in GHC
-
-lemma \<open>unset_bit 13 (473514 :: integer) = 465322\<close>
-  by normalization
-
-test_code \<open>unset_bit 13 (473514 :: integer) = 465322\<close> in GHC
-
-lemma \<open>unset_bit 12 (- 805167 :: integer) = - 809263\<close>
-  by normalization
-
-test_code \<open>unset_bit 12 (- 805167 :: integer) = - 809263\<close> in GHC
-
-lemma \<open>flip_bit 15 (473514 :: integer) = 506282\<close>
-  by normalization
-
-test_code \<open>flip_bit 15 (473514 :: integer) = 506282\<close> in GHC
-
-lemma \<open>flip_bit 12 (- 805167 :: integer) = - 809263\<close>
-  by normalization
-
-test_code \<open>flip_bit 12 (- 805167 :: integer) = - 809263\<close> in GHC
-
-lemma \<open>push_bit 12 (473514 :: integer) = 1939513344\<close>
-  by normalization
-
-test_code \<open>push_bit 12 (473514 :: integer) = 1939513344\<close> in GHC
-
-lemma \<open>push_bit 12 (- 805167 :: integer) = - 3297964032\<close>
-  by normalization
-
-test_code \<open>push_bit 12 (- 805167 :: integer) = - 3297964032\<close> in GHC
-
-lemma \<open>drop_bit 12 (473514 :: integer) = 115\<close>
-  by normalization
-
-test_code \<open>drop_bit 12 (473514 :: integer) = 115\<close> in GHC
-
-lemma \<open>drop_bit 12 (- 805167 :: integer) = - 197\<close>
-  by normalization
-
-test_code \<open>drop_bit 12 (- 805167 :: integer) = - 197\<close> in GHC
-
-lemma \<open>take_bit 12 (473514 :: integer) = 2474\<close>
-  by normalization
-
-test_code \<open>take_bit 12 (473514 :: integer) = 2474\<close> in GHC
-
-lemma \<open>take_bit 12 (- 805167 :: integer) = 1745\<close>
-  by normalization
-
-test_code \<open>take_bit 12 (- 805167 :: integer) = 1745\<close> in GHC
-
-lemma \<open>signed_take_bit 12 (473514 :: integer) = - 1622\<close>
-  by normalization
-
-test_code \<open>signed_take_bit 12 (473514 :: integer) = - 1622\<close> in GHC
-
-lemma \<open>signed_take_bit 12 (- 805167 :: integer) = - 2351\<close>
-  by normalization
-
-test_code \<open>signed_take_bit 12 (- 805167 :: integer) = - 2351\<close> in GHC
-
 end
--- a/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy	Fri Jan 17 20:30:01 2025 +0100
+++ b/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy	Fri Jan 17 21:30:08 2025 +0100
@@ -26,163 +26,4 @@
 
 test_code "stake 10 (cycle ''ab'') = ''ababababab''" in OCaml
 
-text \<open>Test cases for bit operations on target language numerals\<close>
-
-unbundle bit_operations_syntax
-
-lemma \<open>bit (473514 :: integer) 5\<close>
-  by normalization
-
-test_code \<open>bit (473514 :: integer) 5\<close> in OCaml
-
-lemma \<open>bit (- 805167 :: integer) 7\<close>
-  by normalization
-
-test_code \<open>bit (- 805167 :: integer) 7\<close> in OCaml
-
-lemma \<open>473514 AND (767063 :: integer) = 208898\<close>
-  by normalization
-
-test_code \<open>473514 AND (767063 :: integer) = 208898\<close> in OCaml
-
-lemma \<open>- 805167 AND (767063 :: integer) = 242769\<close>
-  by normalization
-
-test_code \<open>- 805167 AND (767063 :: integer) = 242769\<close> in OCaml
-
-lemma \<open>473514 AND (- 314527 :: integer) = 209184\<close>
-  by normalization
-
-test_code \<open>473514 AND (- 314527 :: integer) = 209184\<close> in OCaml
-
-lemma \<open>- 805167 AND (- 314527 :: integer) = - 839103\<close>
-  by normalization
-
-test_code \<open>- 805167 AND (- 314527 :: integer) = - 839103\<close> in OCaml
-
-lemma \<open>473514 OR (767063 :: integer) = 1031679\<close>
-  by normalization
-
-test_code \<open>473514 OR (767063 :: integer) = 1031679\<close> in OCaml
-
-lemma \<open>- 805167 OR (767063 :: integer) = - 280873\<close>
-  by normalization
-
-test_code \<open>- 805167 OR (767063 :: integer) = - 280873\<close> in OCaml
-
-lemma \<open>473514 OR (- 314527 :: integer) = - 50197\<close>
-  by normalization
-
-test_code \<open>473514 OR (- 314527 :: integer) = - 50197\<close> in OCaml
-
-lemma \<open>- 805167 OR (- 314527 :: integer) = - 280591\<close>
-  by normalization
-
-test_code \<open>- 805167 OR (- 314527 :: integer) = - 280591\<close> in OCaml
-
-lemma \<open>473514 XOR (767063 :: integer) = 822781\<close>
-  by normalization
-
-test_code \<open>473514 XOR (767063 :: integer) = 822781\<close> in OCaml
-
-lemma \<open>- 805167 XOR (767063 :: integer) = - 523642\<close>
-  by normalization
-
-test_code \<open>- 805167 XOR (767063 :: integer) = - 523642\<close> in OCaml
-
-lemma \<open>473514 XOR (- 314527 :: integer) = - 259381\<close>
-  by normalization
-
-test_code \<open>473514 XOR (- 314527 :: integer) = - 259381\<close> in OCaml
-
-lemma \<open>- 805167 XOR (- 314527 :: integer) = 558512\<close>
-  by normalization
-
-test_code \<open>- 805167 XOR (- 314527 :: integer) = 558512\<close> in OCaml
-
-lemma \<open>NOT (473513 :: integer) = - 473514\<close>
-  by normalization
-
-test_code \<open>NOT (473513 :: integer) = - 473514\<close> in OCaml
-
-lemma \<open>NOT (- 805167 :: integer) = 805166\<close>
-  by normalization
-
-test_code \<open>NOT (- 805167 :: integer) = 805166\<close> in OCaml
-
-lemma \<open>(mask 39 :: integer) = 549755813887\<close>
-  by normalization
-
-test_code \<open>(mask 39 :: integer) = 549755813887\<close> in OCaml
-
-lemma \<open>set_bit 15 (473514 :: integer) = 506282\<close>
-  by normalization
-
-test_code \<open>set_bit 15 (473514 :: integer) = 506282\<close> in OCaml
-
-lemma \<open>set_bit 11 (- 805167 :: integer) = - 803119\<close>
-  by normalization
-
-test_code \<open>set_bit 11 (- 805167 :: integer) = - 803119\<close> in OCaml
-
-lemma \<open>unset_bit 13 (473514 :: integer) = 465322\<close>
-  by normalization
-
-test_code \<open>unset_bit 13 (473514 :: integer) = 465322\<close> in OCaml
-
-lemma \<open>unset_bit 12 (- 805167 :: integer) = - 809263\<close>
-  by normalization
-
-test_code \<open>unset_bit 12 (- 805167 :: integer) = - 809263\<close> in OCaml
-
-lemma \<open>flip_bit 15 (473514 :: integer) = 506282\<close>
-  by normalization
-
-test_code \<open>flip_bit 15 (473514 :: integer) = 506282\<close> in OCaml
-
-lemma \<open>flip_bit 12 (- 805167 :: integer) = - 809263\<close>
-  by normalization
-
-test_code \<open>flip_bit 12 (- 805167 :: integer) = - 809263\<close> in OCaml
-
-lemma \<open>push_bit 12 (473514 :: integer) = 1939513344\<close>
-  by normalization
-
-test_code \<open>push_bit 12 (473514 :: integer) = 1939513344\<close> in OCaml
-
-lemma \<open>push_bit 12 (- 805167 :: integer) = - 3297964032\<close>
-  by normalization
-
-test_code \<open>push_bit 12 (- 805167 :: integer) = - 3297964032\<close> in OCaml
-
-lemma \<open>drop_bit 12 (473514 :: integer) = 115\<close>
-  by normalization
-
-test_code \<open>drop_bit 12 (473514 :: integer) = 115\<close> in OCaml
-
-lemma \<open>drop_bit 12 (- 805167 :: integer) = - 197\<close>
-  by normalization
-
-test_code \<open>drop_bit 12 (- 805167 :: integer) = - 197\<close> in OCaml
-
-lemma \<open>take_bit 12 (473514 :: integer) = 2474\<close>
-  by normalization
-
-test_code \<open>take_bit 12 (473514 :: integer) = 2474\<close> in OCaml
-
-lemma \<open>take_bit 12 (- 805167 :: integer) = 1745\<close>
-  by normalization
-
-test_code \<open>take_bit 12 (- 805167 :: integer) = 1745\<close> in OCaml
-
-lemma \<open>signed_take_bit 12 (473514 :: integer) = - 1622\<close>
-  by normalization
-
-test_code \<open>signed_take_bit 12 (473514 :: integer) = - 1622\<close> in OCaml
-
-lemma \<open>signed_take_bit 12 (- 805167 :: integer) = - 2351\<close>
-  by normalization
-
-test_code \<open>signed_take_bit 12 (- 805167 :: integer) = - 2351\<close> in OCaml
-
 end
--- a/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy	Fri Jan 17 20:30:01 2025 +0100
+++ b/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy	Fri Jan 17 21:30:08 2025 +0100
@@ -16,163 +16,4 @@
 
 test_code "stake 10 (cycle ''ab'') = ''ababababab''" in PolyML
 
-text \<open>Test cases for bit operations on target language numerals\<close>
-
-unbundle bit_operations_syntax
-
-lemma \<open>bit (473514 :: integer) 5\<close>
-  by normalization
-
-test_code \<open>bit (473514 :: integer) 5\<close> in PolyML
-
-lemma \<open>bit (- 805167 :: integer) 7\<close>
-  by normalization
-
-test_code \<open>bit (- 805167 :: integer) 7\<close> in PolyML
-
-lemma \<open>473514 AND (767063 :: integer) = 208898\<close>
-  by normalization
-
-test_code \<open>473514 AND (767063 :: integer) = 208898\<close> in PolyML
-
-lemma \<open>- 805167 AND (767063 :: integer) = 242769\<close>
-  by normalization
-
-test_code \<open>- 805167 AND (767063 :: integer) = 242769\<close> in PolyML
-
-lemma \<open>473514 AND (- 314527 :: integer) = 209184\<close>
-  by normalization
-
-test_code \<open>473514 AND (- 314527 :: integer) = 209184\<close> in PolyML
-
-lemma \<open>- 805167 AND (- 314527 :: integer) = - 839103\<close>
-  by normalization
-
-test_code \<open>- 805167 AND (- 314527 :: integer) = - 839103\<close> in PolyML
-
-lemma \<open>473514 OR (767063 :: integer) = 1031679\<close>
-  by normalization
-
-test_code \<open>473514 OR (767063 :: integer) = 1031679\<close> in PolyML
-
-lemma \<open>- 805167 OR (767063 :: integer) = - 280873\<close>
-  by normalization
-
-test_code \<open>- 805167 OR (767063 :: integer) = - 280873\<close> in PolyML
-
-lemma \<open>473514 OR (- 314527 :: integer) = - 50197\<close>
-  by normalization
-
-test_code \<open>473514 OR (- 314527 :: integer) = - 50197\<close> in PolyML
-
-lemma \<open>- 805167 OR (- 314527 :: integer) = - 280591\<close>
-  by normalization
-
-test_code \<open>- 805167 OR (- 314527 :: integer) = - 280591\<close> in PolyML
-
-lemma \<open>473514 XOR (767063 :: integer) = 822781\<close>
-  by normalization
-
-test_code \<open>473514 XOR (767063 :: integer) = 822781\<close> in PolyML
-
-lemma \<open>- 805167 XOR (767063 :: integer) = - 523642\<close>
-  by normalization
-
-test_code \<open>- 805167 XOR (767063 :: integer) = - 523642\<close> in PolyML
-
-lemma \<open>473514 XOR (- 314527 :: integer) = - 259381\<close>
-  by normalization
-
-test_code \<open>473514 XOR (- 314527 :: integer) = - 259381\<close> in PolyML
-
-lemma \<open>- 805167 XOR (- 314527 :: integer) = 558512\<close>
-  by normalization
-
-test_code \<open>- 805167 XOR (- 314527 :: integer) = 558512\<close> in PolyML
-
-lemma \<open>NOT (473513 :: integer) = - 473514\<close>
-  by normalization
-
-test_code \<open>NOT (473513 :: integer) = - 473514\<close> in PolyML
-
-lemma \<open>NOT (- 805167 :: integer) = 805166\<close>
-  by normalization
-
-test_code \<open>NOT (- 805167 :: integer) = 805166\<close> in PolyML
-
-lemma \<open>(mask 39 :: integer) = 549755813887\<close>
-  by normalization
-
-test_code \<open>(mask 39 :: integer) = 549755813887\<close> in PolyML
-
-lemma \<open>set_bit 15 (473514 :: integer) = 506282\<close>
-  by normalization
-
-test_code \<open>set_bit 15 (473514 :: integer) = 506282\<close> in PolyML
-
-lemma \<open>set_bit 11 (- 805167 :: integer) = - 803119\<close>
-  by normalization
-
-test_code \<open>set_bit 11 (- 805167 :: integer) = - 803119\<close> in PolyML
-
-lemma \<open>unset_bit 13 (473514 :: integer) = 465322\<close>
-  by normalization
-
-test_code \<open>unset_bit 13 (473514 :: integer) = 465322\<close> in PolyML
-
-lemma \<open>unset_bit 12 (- 805167 :: integer) = - 809263\<close>
-  by normalization
-
-test_code \<open>unset_bit 12 (- 805167 :: integer) = - 809263\<close> in PolyML
-
-lemma \<open>flip_bit 15 (473514 :: integer) = 506282\<close>
-  by normalization
-
-test_code \<open>flip_bit 15 (473514 :: integer) = 506282\<close> in PolyML
-
-lemma \<open>flip_bit 12 (- 805167 :: integer) = - 809263\<close>
-  by normalization
-
-test_code \<open>flip_bit 12 (- 805167 :: integer) = - 809263\<close> in PolyML
-
-lemma \<open>push_bit 12 (473514 :: integer) = 1939513344\<close>
-  by normalization
-
-test_code \<open>push_bit 12 (473514 :: integer) = 1939513344\<close> in PolyML
-
-lemma \<open>push_bit 12 (- 805167 :: integer) = - 3297964032\<close>
-  by normalization
-
-test_code \<open>push_bit 12 (- 805167 :: integer) = - 3297964032\<close> in PolyML
-
-lemma \<open>drop_bit 12 (473514 :: integer) = 115\<close>
-  by normalization
-
-test_code \<open>drop_bit 12 (473514 :: integer) = 115\<close> in PolyML
-
-lemma \<open>drop_bit 12 (- 805167 :: integer) = - 197\<close>
-  by normalization
-
-test_code \<open>drop_bit 12 (- 805167 :: integer) = - 197\<close> in PolyML
-
-lemma \<open>take_bit 12 (473514 :: integer) = 2474\<close>
-  by normalization
-
-test_code \<open>take_bit 12 (473514 :: integer) = 2474\<close> in PolyML
-
-lemma \<open>take_bit 12 (- 805167 :: integer) = 1745\<close>
-  by normalization
-
-test_code \<open>take_bit 12 (- 805167 :: integer) = 1745\<close> in PolyML
-
-lemma \<open>signed_take_bit 12 (473514 :: integer) = - 1622\<close>
-  by normalization
-
-test_code \<open>signed_take_bit 12 (473514 :: integer) = - 1622\<close> in PolyML
-
-lemma \<open>signed_take_bit 12 (- 805167 :: integer) = - 2351\<close>
-  by normalization
-
-test_code \<open>signed_take_bit 12 (- 805167 :: integer) = - 2351\<close> in PolyML
-
 end
--- a/src/HOL/Codegenerator_Test/Code_Test_Scala.thy	Fri Jan 17 20:30:01 2025 +0100
+++ b/src/HOL/Codegenerator_Test/Code_Test_Scala.thy	Fri Jan 17 21:30:08 2025 +0100
@@ -26,163 +26,4 @@
 
 test_code "stake 10 (cycle ''ab'') = ''ababababab''" in Scala
 
-text \<open>Test cases for bit operations on target language numerals\<close>
-
-unbundle bit_operations_syntax
-
-lemma \<open>bit (473514 :: integer) 5\<close>
-  by normalization
-
-test_code \<open>bit (473514 :: integer) 5\<close> in Scala
-
-lemma \<open>bit (- 805167 :: integer) 7\<close>
-  by normalization
-
-test_code \<open>bit (- 805167 :: integer) 7\<close> in Scala
-
-lemma \<open>473514 AND (767063 :: integer) = 208898\<close>
-  by normalization
-
-test_code \<open>473514 AND (767063 :: integer) = 208898\<close> in Scala
-
-lemma \<open>- 805167 AND (767063 :: integer) = 242769\<close>
-  by normalization
-
-test_code \<open>- 805167 AND (767063 :: integer) = 242769\<close> in Scala
-
-lemma \<open>473514 AND (- 314527 :: integer) = 209184\<close>
-  by normalization
-
-test_code \<open>473514 AND (- 314527 :: integer) = 209184\<close> in Scala
-
-lemma \<open>- 805167 AND (- 314527 :: integer) = - 839103\<close>
-  by normalization
-
-test_code \<open>- 805167 AND (- 314527 :: integer) = - 839103\<close> in Scala
-
-lemma \<open>473514 OR (767063 :: integer) = 1031679\<close>
-  by normalization
-
-test_code \<open>473514 OR (767063 :: integer) = 1031679\<close> in Scala
-
-lemma \<open>- 805167 OR (767063 :: integer) = - 280873\<close>
-  by normalization
-
-test_code \<open>- 805167 OR (767063 :: integer) = - 280873\<close> in Scala
-
-lemma \<open>473514 OR (- 314527 :: integer) = - 50197\<close>
-  by normalization
-
-test_code \<open>473514 OR (- 314527 :: integer) = - 50197\<close> in Scala
-
-lemma \<open>- 805167 OR (- 314527 :: integer) = - 280591\<close>
-  by normalization
-
-test_code \<open>- 805167 OR (- 314527 :: integer) = - 280591\<close> in Scala
-
-lemma \<open>473514 XOR (767063 :: integer) = 822781\<close>
-  by normalization
-
-test_code \<open>473514 XOR (767063 :: integer) = 822781\<close> in Scala
-
-lemma \<open>- 805167 XOR (767063 :: integer) = - 523642\<close>
-  by normalization
-
-test_code \<open>- 805167 XOR (767063 :: integer) = - 523642\<close> in Scala
-
-lemma \<open>473514 XOR (- 314527 :: integer) = - 259381\<close>
-  by normalization
-
-test_code \<open>473514 XOR (- 314527 :: integer) = - 259381\<close> in Scala
-
-lemma \<open>- 805167 XOR (- 314527 :: integer) = 558512\<close>
-  by normalization
-
-test_code \<open>- 805167 XOR (- 314527 :: integer) = 558512\<close> in Scala
-
-lemma \<open>NOT (473513 :: integer) = - 473514\<close>
-  by normalization
-
-test_code \<open>NOT (473513 :: integer) = - 473514\<close> in Scala
-
-lemma \<open>NOT (- 805167 :: integer) = 805166\<close>
-  by normalization
-
-test_code \<open>NOT (- 805167 :: integer) = 805166\<close> in Scala
-
-lemma \<open>(mask 39 :: integer) = 549755813887\<close>
-  by normalization
-
-test_code \<open>(mask 39 :: integer) = 549755813887\<close> in Scala
-
-lemma \<open>set_bit 15 (473514 :: integer) = 506282\<close>
-  by normalization
-
-test_code \<open>set_bit 15 (473514 :: integer) = 506282\<close> in Scala
-
-lemma \<open>set_bit 11 (- 805167 :: integer) = - 803119\<close>
-  by normalization
-
-test_code \<open>set_bit 11 (- 805167 :: integer) = - 803119\<close> in Scala
-
-lemma \<open>unset_bit 13 (473514 :: integer) = 465322\<close>
-  by normalization
-
-test_code \<open>unset_bit 13 (473514 :: integer) = 465322\<close> in Scala
-
-lemma \<open>unset_bit 12 (- 805167 :: integer) = - 809263\<close>
-  by normalization
-
-test_code \<open>unset_bit 12 (- 805167 :: integer) = - 809263\<close> in Scala
-
-lemma \<open>flip_bit 15 (473514 :: integer) = 506282\<close>
-  by normalization
-
-test_code \<open>flip_bit 15 (473514 :: integer) = 506282\<close> in Scala
-
-lemma \<open>flip_bit 12 (- 805167 :: integer) = - 809263\<close>
-  by normalization
-
-test_code \<open>flip_bit 12 (- 805167 :: integer) = - 809263\<close> in Scala
-
-lemma \<open>push_bit 12 (473514 :: integer) = 1939513344\<close>
-  by normalization
-
-test_code \<open>push_bit 12 (473514 :: integer) = 1939513344\<close> in Scala
-
-lemma \<open>push_bit 12 (- 805167 :: integer) = - 3297964032\<close>
-  by normalization
-
-test_code \<open>push_bit 12 (- 805167 :: integer) = - 3297964032\<close> in Scala
-
-lemma \<open>drop_bit 12 (473514 :: integer) = 115\<close>
-  by normalization
-
-test_code \<open>drop_bit 12 (473514 :: integer) = 115\<close> in Scala
-
-lemma \<open>drop_bit 12 (- 805167 :: integer) = - 197\<close>
-  by normalization
-
-test_code \<open>drop_bit 12 (- 805167 :: integer) = - 197\<close> in Scala
-
-lemma \<open>take_bit 12 (473514 :: integer) = 2474\<close>
-  by normalization
-
-test_code \<open>take_bit 12 (473514 :: integer) = 2474\<close> in Scala
-
-lemma \<open>take_bit 12 (- 805167 :: integer) = 1745\<close>
-  by normalization
-
-test_code \<open>take_bit 12 (- 805167 :: integer) = 1745\<close> in Scala
-
-lemma \<open>signed_take_bit 12 (473514 :: integer) = - 1622\<close>
-  by normalization
-
-test_code \<open>signed_take_bit 12 (473514 :: integer) = - 1622\<close> in Scala
-
-lemma \<open>signed_take_bit 12 (- 805167 :: integer) = - 2351\<close>
-  by normalization
-
-test_code \<open>signed_take_bit 12 (- 805167 :: integer) = - 2351\<close> in Scala
-
 end
--- a/src/HOL/Codegenerator_Test/Generate_Target_Bit_Operations.thy	Fri Jan 17 20:30:01 2025 +0100
+++ b/src/HOL/Codegenerator_Test/Generate_Target_Bit_Operations.thy	Fri Jan 17 21:30:08 2025 +0100
@@ -60,4 +60,24 @@
 test_code check in GHC
 test_code check in Scala
 
+text \<open>Checking the index maximum for \<text>\<open>PolyML\<close>\<close>
+
+definition \<open>check_max = ()\<close>
+
+definition \<open>anchor = (Code_Target_Bit_Shifts.drop_bit, check_max)\<close>
+
+code_printing
+    code_module Check_Max  \<rightharpoonup>
+      (SML) \<open>
+fun check_max max =
+  let
+    val _ = IntInf.~>> (0, max);
+    val _ = ((IntInf.~>> (0, Word.+ (max, Word.fromInt 1)); raise Fail "Bad max") handle Size => ())
+  in () end;
+\<close>
+  | constant check_max \<rightharpoonup>
+      (SML) "check'_max Bit'_Shifts.word'_max'_index"
+
+test_code \<open>snd anchor = ()\<close> in PolyML
+
 end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Code_Bit_Shifts_for_Arithmetic.thy	Fri Jan 17 21:30:08 2025 +0100
@@ -0,0 +1,62 @@
+(*  Title:      HOL/Library/Code_Bit_Shifts_for_Arithmetic.thy
+    Author:     Florian Haftmann, TU Muenchen
+*)
+
+section \<open>Rewrite arithmetic operations to bit-shifts if feasible\<close>
+
+theory Code_Bit_Shifts_for_Arithmetic
+  imports Main
+begin
+
+context semiring_bit_operations
+begin
+
+context
+  includes bit_operations_syntax
+begin
+
+lemma [code_unfold]:
+  \<open>of_bool (odd a) = a AND 1\<close>
+  by (simp add: and_one_eq mod2_eq_if)
+
+lemma [code_unfold]:
+  \<open>even a \<longleftrightarrow> a AND 1 = 0\<close>
+  by (simp add: and_one_eq mod2_eq_if)
+
+lemma [code_unfold]:
+  \<open>2 * a = push_bit 1 a\<close>
+  by (simp add: ac_simps)
+
+lemma [code_unfold]:
+  \<open>a * 2 = push_bit 1 a\<close>
+  by simp
+
+lemma [code_unfold]:
+  \<open>2 ^ n * a = push_bit n a\<close>
+  by (simp add: push_bit_eq_mult ac_simps)
+
+lemma [code_unfold]:
+  \<open>a * 2 ^ n = push_bit n a\<close>
+  by (simp add: push_bit_eq_mult)
+
+lemma [code_unfold]:
+  \<open>a div 2 = drop_bit 1 a\<close>
+  by (simp add: drop_bit_eq_div)
+
+lemma [code_unfold]:
+  \<open>a div 2 ^ n = drop_bit n a\<close>
+  by (simp add: drop_bit_eq_div)
+
+lemma [code_unfold]:
+  \<open>a mod 2 = take_bit 1 a\<close>
+  by (simp add: take_bit_eq_mod)
+
+lemma [code_unfold]:
+  \<open>a mod 2 ^ n  = take_bit n a\<close>
+  by (simp add: take_bit_eq_mod)
+
+end
+
+end
+
+end
--- a/src/HOL/Library/Code_Target_Bit_Shifts.thy	Fri Jan 17 20:30:01 2025 +0100
+++ b/src/HOL/Library/Code_Target_Bit_Shifts.thy	Fri Jan 17 21:30:08 2025 +0100
@@ -41,6 +41,7 @@
   type int = IntInf.int
   val push : int -> int -> int
   val drop : int -> int -> int
+  val word_max_index : Word.word (*only for validation*)
 end = struct
 
 type int = IntInf.int;
--- a/src/HOL/Library/Complete_Partial_Order2.thy	Fri Jan 17 20:30:01 2025 +0100
+++ b/src/HOL/Library/Complete_Partial_Order2.thy	Fri Jan 17 21:30:08 2025 +0100
@@ -13,48 +13,48 @@
 lemma chain_transfer [transfer_rule]:
   includes lifting_syntax
   shows "((A ===> A ===> (=)) ===> rel_set A ===> (=)) Complete_Partial_Order.chain Complete_Partial_Order.chain"
-unfolding chain_def[abs_def] by transfer_prover
-                             
+  unfolding chain_def[abs_def] by transfer_prover
+
 lemma linorder_chain [simp, intro!]:
   fixes Y :: "_ :: linorder set"
   shows "Complete_Partial_Order.chain (\<le>) Y"
-by(auto intro: chainI)
+  by(auto intro: chainI)
 
 lemma fun_lub_apply: "\<And>Sup. fun_lub Sup Y x = Sup ((\<lambda>f. f x) ` Y)"
-by(simp add: fun_lub_def image_def)
+  by(simp add: fun_lub_def image_def)
 
 lemma fun_lub_empty [simp]: "fun_lub lub {} = (\<lambda>_. lub {})"
-by(rule ext)(simp add: fun_lub_apply)
+  by(rule ext)(simp add: fun_lub_apply)
 
 lemma chain_fun_ordD: 
   assumes "Complete_Partial_Order.chain (fun_ord le) Y"
   shows "Complete_Partial_Order.chain le ((\<lambda>f. f x) ` Y)"
-by(rule chainI)(auto dest: chainD[OF assms] simp add: fun_ord_def)
+  by(rule chainI)(auto dest: chainD[OF assms] simp add: fun_ord_def)
 
 lemma chain_Diff:
   "Complete_Partial_Order.chain ord A
   \<Longrightarrow> Complete_Partial_Order.chain ord (A - B)"
-by(erule chain_subset) blast
+  by(erule chain_subset) blast
 
 lemma chain_rel_prodD1:
   "Complete_Partial_Order.chain (rel_prod orda ordb) Y
   \<Longrightarrow> Complete_Partial_Order.chain orda (fst ` Y)"
-by(auto 4 3 simp add: chain_def)
+  by(auto 4 3 simp add: chain_def)
 
 lemma chain_rel_prodD2:
   "Complete_Partial_Order.chain (rel_prod orda ordb) Y
   \<Longrightarrow> Complete_Partial_Order.chain ordb (snd ` Y)"
-by(auto 4 3 simp add: chain_def)
+  by(auto 4 3 simp add: chain_def)
 
 
 context ccpo begin
 
 lemma ccpo_fun: "class.ccpo (fun_lub Sup) (fun_ord (\<le>)) (mk_less (fun_ord (\<le>)))"
   by standard (auto 4 3 simp add: mk_less_def fun_ord_def fun_lub_apply
-    intro: order.trans order.antisym chain_imageI ccpo_Sup_upper ccpo_Sup_least)
+      intro: order.trans order.antisym chain_imageI ccpo_Sup_upper ccpo_Sup_least)
 
 lemma ccpo_Sup_below_iff: "Complete_Partial_Order.chain (\<le>) Y \<Longrightarrow> Sup Y \<le> x \<longleftrightarrow> (\<forall>y\<in>Y. y \<le> x)"
-by(fast intro: order_trans[OF ccpo_Sup_upper] ccpo_Sup_least)
+  by (meson local.ccpo_Sup_least local.ccpo_Sup_upper local.dual_order.trans)
 
 lemma Sup_minus_bot: 
   assumes chain: "Complete_Partial_Order.chain (\<le>) A"
@@ -152,11 +152,9 @@
   proof(rule ccpo_Sup_least)
     fix y
     assume "y \<in> (\<lambda>x. f x x) ` Y"
-    then obtain x where "x \<in> Y" and "y = f x x" by blast note this(2)
-    also from chain2[OF \<open>x \<in> Y\<close>] have "\<dots> \<le> \<Squnion>(f x ` Y)"
-      by(rule ccpo_Sup_upper)(simp add: \<open>x \<in> Y\<close>)
-    also have "\<dots> \<le> ?lhs" by(rule ccpo_Sup_upper[OF chain1])(simp add: \<open>x \<in> Y\<close>)
-    finally show "y \<le> ?lhs" .
+    then obtain x where "x \<in> Y" and "y = f x x" by blast
+    then show "y \<le> ?lhs"
+      by (metis (no_types, lifting) chain1 chain2 imageI ccpo_Sup_upper order.trans)
   qed
 qed
 
@@ -180,6 +178,7 @@
   finally show "x \<le> \<dots>" .
 qed
 
+
 lemma swap_Sup:
   fixes le_b (infix \<open>\<sqsubseteq>\<close> 60)
   assumes Y: "Complete_Partial_Order.chain (\<sqsubseteq>) Y"
@@ -222,11 +221,10 @@
     proof(rule ccpo_Sup_least)
       fix x'
       assume "x' \<in> (\<lambda>f. f x) ` Z"
-      then obtain f where "f \<in> Z" "x' = f x" by blast note this(2)
-      also have "f x \<le> f y" using \<open>f \<in> Z\<close> \<open>x \<sqsubseteq> y\<close> by(rule monotoneD[OF mono])
-      also have "f y \<le> ?rhs" using chain3
-        by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Z\<close>)
-      finally show "x' \<le> ?rhs" .
+      then obtain f where "f \<in> Z" "x' = f x" by blast 
+      then show "x' \<le> ?rhs"
+        by (metis (mono_tags, lifting) \<open>x \<sqsubseteq> y\<close> chain3 imageI ccpo_Sup_upper
+            order_trans mono monotoneD)
     qed
   qed
 
@@ -239,11 +237,10 @@
     proof(rule ccpo_Sup_least)
       fix x'
       assume "x' \<in> f ` Y"
-      then obtain y where "y \<in> Y" "x' = f y" by blast note this(2)
-      also have "f y \<le> \<Squnion>((\<lambda>f. f y) ` Z)" using chain3
-        by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Z\<close>)
-      also have "\<dots> \<le> ?rhs" using chain4 by(rule ccpo_Sup_upper)(simp add: \<open>y \<in> Y\<close>)
-      finally show "x' \<le> ?rhs" .
+      then obtain y where "y \<in> Y" "x' = f y" by blast
+      then show "x' \<le> ?rhs"
+        by (metis (mono_tags, lifting) \<open>f \<in> Z\<close> chain3 chain4 imageI local.ccpo_Sup_upper
+            order.trans)
     qed
     finally show "x \<le> ?rhs" .
   qed
@@ -257,12 +254,10 @@
     proof(rule ccpo_Sup_least)
       fix x'
       assume "x' \<in> (\<lambda>f. f y) ` Z"
-      then obtain f where "f \<in> Z" "x' = f y" by blast note this(2)
-      also have "f y \<le> \<Squnion>(f ` Y)" using chain1[OF \<open>f \<in> Z\<close>]
-        by(rule ccpo_Sup_upper)(simp add: \<open>y \<in> Y\<close>)
-      also have "\<dots> \<le> ?lhs" using chain2
-        by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Z\<close>)
-      finally show "x' \<le> ?lhs" .
+      then obtain f where "f \<in> Z" "x' = f y" by blast
+      then show "x' \<le> ?lhs"
+        by (metis (mono_tags, lifting) \<open>y \<in> Y\<close> ccpo_Sup_below_iff chain1 chain2 imageI
+            ccpo_Sup_upper)
     qed
     finally show "x \<le> ?lhs" .
   qed
@@ -411,47 +406,47 @@
 declare if_mono[simp]
 
 lemma monotone_id' [cont_intro]: "monotone ord ord (\<lambda>x. x)"
-by(simp add: monotone_def)
+  by(simp add: monotone_def)
 
 lemma monotone_applyI:
   "monotone orda ordb F \<Longrightarrow> monotone (fun_ord orda) ordb (\<lambda>f. F (f x))"
-by(rule monotoneI)(auto simp add: fun_ord_def dest: monotoneD)
+  by(rule monotoneI)(auto simp add: fun_ord_def dest: monotoneD)
 
 lemma monotone_if_fun [partial_function_mono]:
   "\<lbrakk> monotone (fun_ord orda) (fun_ord ordb) F; monotone (fun_ord orda) (fun_ord ordb) G \<rbrakk>
   \<Longrightarrow> monotone (fun_ord orda) (fun_ord ordb) (\<lambda>f n. if c n then F f n else G f n)"
-by(simp add: monotone_def fun_ord_def)
+  by(simp add: monotone_def fun_ord_def)
 
 lemma monotone_fun_apply_fun [partial_function_mono]: 
   "monotone (fun_ord (fun_ord ord)) (fun_ord ord) (\<lambda>f n. f t (g n))"
-by(rule monotoneI)(simp add: fun_ord_def)
+  by(rule monotoneI)(simp add: fun_ord_def)
 
 lemma monotone_fun_ord_apply: 
   "monotone orda (fun_ord ordb) f \<longleftrightarrow> (\<forall>x. monotone orda ordb (\<lambda>y. f y x))"
-by(auto simp add: monotone_def fun_ord_def)
+  by(auto simp add: monotone_def fun_ord_def)
 
 context preorder begin
 
 declare transp_on_le[cont_intro]
 
 lemma monotone_const [simp, cont_intro]: "monotone ord (\<le>) (\<lambda>_. c)"
-by(rule monotoneI) simp
+  by(rule monotoneI) simp
 
 end
 
 lemma transp_le [cont_intro, simp]:
   "class.preorder ord (mk_less ord) \<Longrightarrow> transp ord"
-by(rule preorder.transp_on_le)
+  by(rule preorder.transp_on_le)
 
 context partial_function_definitions begin
 
 declare const_mono [cont_intro, simp]
 
 lemma transp_le [cont_intro, simp]: "transp leq"
-by(rule transpI)(rule leq_trans)
+  by(rule transpI)(rule leq_trans)
 
 lemma preorder [cont_intro, simp]: "class.preorder leq (mk_less leq)"
-by(unfold_locales)(auto simp add: mk_less_def intro: leq_refl leq_trans)
+  by(unfold_locales)(auto simp add: mk_less_def intro: leq_refl leq_trans)
 
 declare ccpo[cont_intro, simp]
 
@@ -460,91 +455,91 @@
 lemma contI [intro?]:
   "(\<And>Y. \<lbrakk> Complete_Partial_Order.chain orda Y; Y \<noteq> {} \<rbrakk> \<Longrightarrow> f (luba Y) = lubb (f ` Y)) 
   \<Longrightarrow> cont luba orda lubb ordb f"
-unfolding cont_def by blast
+  unfolding cont_def by blast
 
 lemma contD:
   "\<lbrakk> cont luba orda lubb ordb f; Complete_Partial_Order.chain orda Y; Y \<noteq> {} \<rbrakk> 
   \<Longrightarrow> f (luba Y) = lubb (f ` Y)"
-unfolding cont_def by blast
+  unfolding cont_def by blast
 
 lemma cont_id [simp, cont_intro]: "\<And>Sup. cont Sup ord Sup ord id"
-by(rule contI) simp
+  by(rule contI) simp
 
 lemma cont_id' [simp, cont_intro]: "\<And>Sup. cont Sup ord Sup ord (\<lambda>x. x)"
-using cont_id[unfolded id_def] .
+  using cont_id[unfolded id_def] .
 
 lemma cont_applyI [cont_intro]:
   assumes cont: "cont luba orda lubb ordb g"
   shows "cont (fun_lub luba) (fun_ord orda) lubb ordb (\<lambda>f. g (f x))"
-by(rule contI)(drule chain_fun_ordD[where x=x], simp add: fun_lub_apply image_image contD[OF cont])
+  by(rule contI)(drule chain_fun_ordD[where x=x], simp add: fun_lub_apply image_image contD[OF cont])
 
 lemma call_cont: "cont (fun_lub lub) (fun_ord ord) lub ord (\<lambda>f. f t)"
-by(simp add: cont_def fun_lub_apply)
+  by(simp add: cont_def fun_lub_apply)
 
 lemma cont_if [cont_intro]:
   "\<lbrakk> cont luba orda lubb ordb f; cont luba orda lubb ordb g \<rbrakk>
   \<Longrightarrow> cont luba orda lubb ordb (\<lambda>x. if c then f x else g x)"
-by(cases c) simp_all
+  by(cases c) simp_all
 
 lemma mcontI [intro?]:
-   "\<lbrakk> monotone orda ordb f; cont luba orda lubb ordb f \<rbrakk> \<Longrightarrow> mcont luba orda lubb ordb f"
-by(simp add: mcont_def)
+  "\<lbrakk> monotone orda ordb f; cont luba orda lubb ordb f \<rbrakk> \<Longrightarrow> mcont luba orda lubb ordb f"
+  by(simp add: mcont_def)
 
 lemma mcont_mono: "mcont luba orda lubb ordb f \<Longrightarrow> monotone orda ordb f"
-by(simp add: mcont_def)
+  by(simp add: mcont_def)
 
 lemma mcont_cont [simp]: "mcont luba orda lubb ordb f \<Longrightarrow> cont luba orda lubb ordb f"
-by(simp add: mcont_def)
+  by(simp add: mcont_def)
 
 lemma mcont_monoD:
   "\<lbrakk> mcont luba orda lubb ordb f; orda x y \<rbrakk> \<Longrightarrow> ordb (f x) (f y)"
-by(auto simp add: mcont_def dest: monotoneD)
+  by(auto simp add: mcont_def dest: monotoneD)
 
 lemma mcont_contD:
   "\<lbrakk> mcont luba orda lubb ordb f; Complete_Partial_Order.chain orda Y; Y \<noteq> {} \<rbrakk>
   \<Longrightarrow> f (luba Y) = lubb (f ` Y)"
-by(auto simp add: mcont_def dest: contD)
+  by(auto simp add: mcont_def dest: contD)
 
 lemma mcont_call [cont_intro, simp]:
   "mcont (fun_lub lub) (fun_ord ord) lub ord (\<lambda>f. f t)"
-by(simp add: mcont_def call_mono call_cont)
+  by(simp add: mcont_def call_mono call_cont)
 
 lemma mcont_id' [cont_intro, simp]: "mcont lub ord lub ord (\<lambda>x. x)"
-by(simp add: mcont_def monotone_id')
+  by(simp add: mcont_def monotone_id')
 
 lemma mcont_applyI:
   "mcont luba orda lubb ordb (\<lambda>x. F x) \<Longrightarrow> mcont (fun_lub luba) (fun_ord orda) lubb ordb (\<lambda>f. F (f x))"
-by(simp add: mcont_def monotone_applyI cont_applyI)
+  by(simp add: mcont_def monotone_applyI cont_applyI)
 
 lemma mcont_if [cont_intro, simp]:
   "\<lbrakk> mcont luba orda lubb ordb (\<lambda>x. f x); mcont luba orda lubb ordb (\<lambda>x. g x) \<rbrakk>
   \<Longrightarrow> mcont luba orda lubb ordb (\<lambda>x. if c then f x else g x)"
-by(simp add: mcont_def cont_if)
+  by(simp add: mcont_def cont_if)
 
 lemma cont_fun_lub_apply: 
   "cont luba orda (fun_lub lubb) (fun_ord ordb) f \<longleftrightarrow> (\<forall>x. cont luba orda lubb ordb (\<lambda>y. f y x))"
-by(simp add: cont_def fun_lub_def fun_eq_iff)(auto simp add: image_def)
+  by(simp add: cont_def fun_lub_def fun_eq_iff)(auto simp add: image_def)
 
 lemma mcont_fun_lub_apply: 
   "mcont luba orda (fun_lub lubb) (fun_ord ordb) f \<longleftrightarrow> (\<forall>x. mcont luba orda lubb ordb (\<lambda>y. f y x))"
-by(auto simp add: monotone_fun_ord_apply cont_fun_lub_apply mcont_def)
+  by(auto simp add: monotone_fun_ord_apply cont_fun_lub_apply mcont_def)
 
 context ccpo begin
 
 lemma cont_const [simp, cont_intro]: "cont luba orda Sup (\<le>) (\<lambda>x. c)"
-by (rule contI) (simp add: image_constant_conv cong del: SUP_cong_simp)
+  by (rule contI) (simp add: image_constant_conv cong del: SUP_cong_simp)
 
 lemma mcont_const [cont_intro, simp]:
   "mcont luba orda Sup (\<le>) (\<lambda>x. c)"
-by(simp add: mcont_def)
+  by(simp add: mcont_def)
 
 lemma cont_apply:
   assumes 2: "\<And>x. cont lubb ordb Sup (\<le>) (\<lambda>y. f x y)"
-  and t: "cont luba orda lubb ordb (\<lambda>x. t x)"
-  and 1: "\<And>y. cont luba orda Sup (\<le>) (\<lambda>x. f x y)"
-  and mono: "monotone orda ordb (\<lambda>x. t x)"
-  and mono2: "\<And>x. monotone ordb (\<le>) (\<lambda>y. f x y)"
-  and mono1: "\<And>y. monotone orda (\<le>) (\<lambda>x. f x y)"
+    and t: "cont luba orda lubb ordb (\<lambda>x. t x)"
+    and 1: "\<And>y. cont luba orda Sup (\<le>) (\<lambda>x. f x y)"
+    and mono: "monotone orda ordb (\<lambda>x. t x)"
+    and mono2: "\<And>x. monotone ordb (\<le>) (\<lambda>y. f x y)"
+    and mono1: "\<And>y. monotone orda (\<le>) (\<lambda>x. f x y)"
   shows "cont luba orda Sup (\<le>) (\<lambda>x. f x (t x))"
 proof
   fix Y
@@ -561,16 +556,16 @@
      \<And>y. mcont lub ord Sup (\<le>) (\<lambda>x. f x y);
      mcont lub ord lub' ord' (\<lambda>y. t y) \<rbrakk>
   \<Longrightarrow> mcont lub ord Sup (\<le>) (\<lambda>x. f x (t x))"
-unfolding mcont_def by(blast intro: transp_on_le monotone2monotone cont_apply)
+  unfolding mcont_def by(blast intro: transp_on_le monotone2monotone cont_apply)
 
 lemma mcont2mcont:
   "\<lbrakk>mcont lub' ord' Sup (\<le>) (\<lambda>x. f x); mcont lub ord lub' ord' (\<lambda>x. t x)\<rbrakk> 
   \<Longrightarrow> mcont lub ord Sup (\<le>) (\<lambda>x. f (t x))"
-by(rule mcont2mcont'[OF _ mcont_const]) 
+  by(rule mcont2mcont'[OF _ mcont_const]) 
 
 context
   fixes ord :: "'b \<Rightarrow> 'b \<Rightarrow> bool" (infix \<open>\<sqsubseteq>\<close> 60) 
-  and lub :: "'b set \<Rightarrow> 'b" (\<open>\<Or>\<close>)
+    and lub :: "'b set \<Rightarrow> 'b" (\<open>\<Or>\<close>)
 begin
 
 lemma cont_fun_lub_Sup:
@@ -818,42 +813,42 @@
 lemma admissible_disj' [simp, cont_intro]:
   "\<lbrakk> class.ccpo lub ord (mk_less ord); ccpo.admissible lub ord P; ccpo.admissible lub ord Q \<rbrakk>
   \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. P x \<or> Q x)"
-by(rule ccpo.admissible_disj)
+  by(rule ccpo.admissible_disj)
 
 lemma admissible_imp' [cont_intro]:
   "\<lbrakk> class.ccpo lub ord (mk_less ord);
      ccpo.admissible lub ord (\<lambda>x. \<not> P x);
      ccpo.admissible lub ord (\<lambda>x. Q x) \<rbrakk>
   \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. P x \<longrightarrow> Q x)"
-unfolding imp_conv_disj by(rule ccpo.admissible_disj)
+  unfolding imp_conv_disj by(rule ccpo.admissible_disj)
 
 lemma admissible_imp [cont_intro]:
   "(Q \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. P x))
   \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. Q \<longrightarrow> P x)"
-by(rule ccpo.admissibleI)(auto dest: ccpo.admissibleD)
+  by(rule ccpo.admissibleI)(auto dest: ccpo.admissibleD)
 
 lemma admissible_not_mem' [THEN admissible_subst, cont_intro, simp]:
   shows admissible_not_mem: "ccpo.admissible Union (\<subseteq>) (\<lambda>A. x \<notin> A)"
-by(rule ccpo.admissibleI) auto
+  by(rule ccpo.admissibleI) auto
 
 lemma admissible_eqI:
   assumes f: "cont luba orda lub ord (\<lambda>x. f x)"
-  and g: "cont luba orda lub ord (\<lambda>x. g x)"
+    and g: "cont luba orda lub ord (\<lambda>x. g x)"
   shows "ccpo.admissible luba orda (\<lambda>x. f x = g x)"
-apply(rule ccpo.admissibleI)
-apply(simp_all add: contD[OF f] contD[OF g] cong: image_cong)
-done
+  apply(rule ccpo.admissibleI)
+  apply(simp_all add: contD[OF f] contD[OF g] cong: image_cong)
+  done
 
 corollary admissible_eq_mcontI [cont_intro]:
   "\<lbrakk> mcont luba orda lub ord (\<lambda>x. f x); 
     mcont luba orda lub ord (\<lambda>x. g x) \<rbrakk>
   \<Longrightarrow> ccpo.admissible luba orda (\<lambda>x. f x = g x)"
-by(rule admissible_eqI)(auto simp add: mcont_def)
+  by(rule admissible_eqI)(auto simp add: mcont_def)
 
 lemma admissible_iff [cont_intro, simp]:
   "\<lbrakk> ccpo.admissible lub ord (\<lambda>x. P x \<longrightarrow> Q x); ccpo.admissible lub ord (\<lambda>x. Q x \<longrightarrow> P x) \<rbrakk>
   \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. P x \<longleftrightarrow> Q x)"
-by(subst iff_conv_conj_imp)(rule admissible_conj)
+  by(subst iff_conv_conj_imp)(rule admissible_conj)
 
 context ccpo begin
 
@@ -999,35 +994,35 @@
     and bot: "P (\<lambda>_. lub {})"
     and step: "\<And>f'. \<lbrakk> P (U f'); le_fun (U f') (U f) \<rbrakk> \<Longrightarrow> P (U (F f'))"
   shows "P (U f)"
-unfolding eq inverse
-apply (rule ccpo.fixp_strong_induct[OF ccpo adm])
-apply (insert mono, auto simp: monotone_def fun_ord_def bot fun_lub_def)[2]
-apply (rule_tac f'5="C x" in step)
-apply (simp_all add: inverse eq)
-done
+  unfolding eq inverse
+  apply (rule ccpo.fixp_strong_induct[OF ccpo adm])
+    apply (insert mono, auto simp: monotone_def fun_ord_def bot fun_lub_def)[2]
+  apply (rule_tac f'5="C x" in step)
+   apply (simp_all add: inverse eq)
+  done
 
 end
 
 subsection \<open>\<^term>\<open>(=)\<close> as order\<close>
 
 definition lub_singleton :: "('a set \<Rightarrow> 'a) \<Rightarrow> bool"
-where "lub_singleton lub \<longleftrightarrow> (\<forall>a. lub {a} = a)"
+  where "lub_singleton lub \<longleftrightarrow> (\<forall>a. lub {a} = a)"
 
 definition the_Sup :: "'a set \<Rightarrow> 'a"
-where "the_Sup A = (THE a. a \<in> A)"
+  where "the_Sup A = (THE a. a \<in> A)"
 
 lemma lub_singleton_the_Sup [cont_intro, simp]: "lub_singleton the_Sup"
-by(simp add: lub_singleton_def the_Sup_def)
+  by(simp add: lub_singleton_def the_Sup_def)
 
 lemma (in ccpo) lub_singleton: "lub_singleton Sup"
-by(simp add: lub_singleton_def)
+  by(simp add: lub_singleton_def)
 
 lemma (in partial_function_definitions) lub_singleton [cont_intro, simp]: "lub_singleton lub"
-by(rule ccpo.lub_singleton)(rule Partial_Function.ccpo[OF partial_function_definitions_axioms])
+  by(rule ccpo.lub_singleton)(rule Partial_Function.ccpo[OF partial_function_definitions_axioms])
 
 lemma preorder_eq [cont_intro, simp]:
   "class.preorder (=) (mk_less (=))"
-by(unfold_locales)(simp_all add: mk_less_def)
+  by(unfold_locales)(simp_all add: mk_less_def)
 
 lemma monotone_eqI [cont_intro]:
   assumes "class.preorder ord (mk_less ord)"
@@ -1052,23 +1047,23 @@
 lemma mcont_eqI [cont_intro, simp]:
   "\<lbrakk> class.preorder ord (mk_less ord); lub_singleton lub \<rbrakk>
   \<Longrightarrow> mcont the_Sup (=) lub ord f"
-by(simp add: mcont_def cont_eqI monotone_eqI)
+  by(simp add: mcont_def cont_eqI monotone_eqI)
 
 subsection \<open>ccpo for products\<close>
 
 definition prod_lub :: "('a set \<Rightarrow> 'a) \<Rightarrow> ('b set \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'b) set \<Rightarrow> 'a \<times> 'b"
-where "prod_lub Sup_a Sup_b Y = (Sup_a (fst ` Y), Sup_b (snd ` Y))"
+  where "prod_lub Sup_a Sup_b Y = (Sup_a (fst ` Y), Sup_b (snd ` Y))"
 
 lemma lub_singleton_prod_lub [cont_intro, simp]:
   "\<lbrakk> lub_singleton luba; lub_singleton lubb \<rbrakk> \<Longrightarrow> lub_singleton (prod_lub luba lubb)"
-by(simp add: lub_singleton_def prod_lub_def)
+  by(simp add: lub_singleton_def prod_lub_def)
 
 lemma prod_lub_empty [simp]: "prod_lub luba lubb {} = (luba {}, lubb {})"
-by(simp add: prod_lub_def)
+  by(simp add: prod_lub_def)
 
 lemma preorder_rel_prodI [cont_intro, simp]:
   assumes "class.preorder orda (mk_less orda)"
-  and "class.preorder ordb (mk_less ordb)"
+    and "class.preorder ordb (mk_less ordb)"
   shows "class.preorder (rel_prod orda ordb) (mk_less (rel_prod orda ordb))"
 proof -
   interpret a: preorder orda "mk_less orda" by fact
@@ -1078,9 +1073,9 @@
 
 lemma order_rel_prodI:
   assumes a: "class.order orda (mk_less orda)"
-  and b: "class.order ordb (mk_less ordb)"
+    and b: "class.order ordb (mk_less ordb)"
   shows "class.order (rel_prod orda ordb) (mk_less (rel_prod orda ordb))"
-  (is "class.order ?ord ?ord'")
+    (is "class.order ?ord ?ord'")
 proof(intro class.order.intro class.order_axioms.intro)
   interpret a: order orda "mk_less orda" by(fact a)
   interpret b: order ordb "mk_less ordb" by(fact b)
@@ -1093,10 +1088,10 @@
 
 lemma monotone_rel_prodI:
   assumes mono2: "\<And>a. monotone ordb ordc (\<lambda>b. f (a, b))"
-  and mono1: "\<And>b. monotone orda ordc (\<lambda>a. f (a, b))"
-  and a: "class.preorder orda (mk_less orda)"
-  and b: "class.preorder ordb (mk_less ordb)"
-  and c: "class.preorder ordc (mk_less ordc)"
+    and mono1: "\<And>b. monotone orda ordc (\<lambda>a. f (a, b))"
+    and a: "class.preorder orda (mk_less orda)"
+    and b: "class.preorder ordb (mk_less ordb)"
+    and c: "class.preorder ordc (mk_less ordc)"
   shows "monotone (rel_prod orda ordb) ordc f"
 proof -
   interpret a: preorder orda "mk_less orda" by(rule a)
@@ -1108,7 +1103,7 @@
 
 lemma monotone_rel_prodD1:
   assumes mono: "monotone (rel_prod orda ordb) ordc f"
-  and preorder: "class.preorder ordb (mk_less ordb)"
+    and preorder: "class.preorder ordb (mk_less ordb)"
   shows "monotone orda ordc (\<lambda>a. f (a, b))"
 proof -
   interpret preorder ordb "mk_less ordb" by(rule preorder)
@@ -1117,7 +1112,7 @@
 
 lemma monotone_rel_prodD2:
   assumes mono: "monotone (rel_prod orda ordb) ordc f"
-  and preorder: "class.preorder orda (mk_less orda)"
+    and preorder: "class.preorder orda (mk_less orda)"
   shows "monotone ordb ordc (\<lambda>b. f (a, b))"
 proof -
   interpret preorder orda "mk_less orda" by(rule preorder)
@@ -1129,68 +1124,68 @@
     class.preorder orda (mk_less orda); class.preorder ordb (mk_less ordb);
     class.preorder ordc (mk_less ordc) \<rbrakk>
   \<Longrightarrow> monotone (rel_prod orda ordb) ordc (case_prod f)"
-by(rule monotone_rel_prodI) simp_all
+  by(rule monotone_rel_prodI) simp_all
 
 lemma monotone_case_prodD1:
   assumes mono: "monotone (rel_prod orda ordb) ordc (case_prod f)"
-  and preorder: "class.preorder ordb (mk_less ordb)"
+    and preorder: "class.preorder ordb (mk_less ordb)"
   shows "monotone orda ordc (\<lambda>a. f a b)"
-using monotone_rel_prodD1[OF assms] by simp
+  using monotone_rel_prodD1[OF assms] by simp
 
 lemma monotone_case_prodD2:
   assumes mono: "monotone (rel_prod orda ordb) ordc (case_prod f)"
-  and preorder: "class.preorder orda (mk_less orda)"
+    and preorder: "class.preorder orda (mk_less orda)"
   shows "monotone ordb ordc (f a)"
-using monotone_rel_prodD2[OF assms] by simp
+  using monotone_rel_prodD2[OF assms] by simp
 
 context 
   fixes orda ordb ordc
   assumes a: "class.preorder orda (mk_less orda)"
-  and b: "class.preorder ordb (mk_less ordb)"
-  and c: "class.preorder ordc (mk_less ordc)"
+    and b: "class.preorder ordb (mk_less ordb)"
+    and c: "class.preorder ordc (mk_less ordc)"
 begin
 
 lemma monotone_rel_prod_iff:
   "monotone (rel_prod orda ordb) ordc f \<longleftrightarrow>
    (\<forall>a. monotone ordb ordc (\<lambda>b. f (a, b))) \<and> 
    (\<forall>b. monotone orda ordc (\<lambda>a. f (a, b)))"
-using a b c by(blast intro: monotone_rel_prodI dest: monotone_rel_prodD1 monotone_rel_prodD2)
+  using a b c by(blast intro: monotone_rel_prodI dest: monotone_rel_prodD1 monotone_rel_prodD2)
 
 lemma monotone_case_prod_iff [simp]:
   "monotone (rel_prod orda ordb) ordc (case_prod f) \<longleftrightarrow>
    (\<forall>a. monotone ordb ordc (f a)) \<and> (\<forall>b. monotone orda ordc (\<lambda>a. f a b))"
-by(simp add: monotone_rel_prod_iff)
+  by(simp add: monotone_rel_prod_iff)
 
 end
 
 lemma monotone_case_prod_apply_iff:
   "monotone orda ordb (\<lambda>x. (case_prod f x) y) \<longleftrightarrow> monotone orda ordb (case_prod (\<lambda>a b. f a b y))"
-by(simp add: monotone_def)
+  by(simp add: monotone_def)
 
 lemma monotone_case_prod_applyD:
   "monotone orda ordb (\<lambda>x. (case_prod f x) y)
   \<Longrightarrow> monotone orda ordb (case_prod (\<lambda>a b. f a b y))"
-by(simp add: monotone_case_prod_apply_iff)
+  by(simp add: monotone_case_prod_apply_iff)
 
 lemma monotone_case_prod_applyI:
   "monotone orda ordb (case_prod (\<lambda>a b. f a b y))
   \<Longrightarrow> monotone orda ordb (\<lambda>x. (case_prod f x) y)"
-by(simp add: monotone_case_prod_apply_iff)
+  by(simp add: monotone_case_prod_apply_iff)
 
 
 lemma cont_case_prod_apply_iff:
   "cont luba orda lubb ordb (\<lambda>x. (case_prod f x) y) \<longleftrightarrow> cont luba orda lubb ordb (case_prod (\<lambda>a b. f a b y))"
-by(simp add: cont_def split_def)
+  by(simp add: cont_def split_def)
 
 lemma cont_case_prod_applyI:
   "cont luba orda lubb ordb (case_prod (\<lambda>a b. f a b y))
   \<Longrightarrow> cont luba orda lubb ordb (\<lambda>x. (case_prod f x) y)"
-by(simp add: cont_case_prod_apply_iff)
+  by(simp add: cont_case_prod_apply_iff)
 
 lemma cont_case_prod_applyD:
   "cont luba orda lubb ordb (\<lambda>x. (case_prod f x) y)
   \<Longrightarrow> cont luba orda lubb ordb (case_prod (\<lambda>a b. f a b y))"
-by(simp add: cont_case_prod_apply_iff)
+  by(simp add: cont_case_prod_apply_iff)
 
 lemma mcont_case_prod_apply_iff [simp]:
   "mcont luba orda lubb ordb (\<lambda>x. (case_prod f x) y) \<longleftrightarrow> 
@@ -1307,13 +1302,8 @@
   and t: "monotone orda ordb (\<lambda>x. t x)"
   and t': "monotone orda ordc (\<lambda>x. t' x)"
   shows "monotone orda leq (\<lambda>x. f (t x) (t' x))"
-proof(rule monotoneI)
-  fix x y
-  assume "orda x y"
-  hence "rel_prod ordb ordc (t x, t' x) (t y, t' y)"
-    using t t' by(auto dest: monotoneD)
-  from monotoneD[OF f this] show "leq (f (t x) (t' x)) (f (t y) (t' y))" by simp
-qed
+  by (metis (mono_tags, lifting) case_prod_conv monotoneD monotoneI rel_prod.intros
+      assms)
 
 lemma cont_case_prodI [cont_intro]:
   "\<lbrakk> monotone (rel_prod orda ordb) leq (case_prod f);
@@ -1322,7 +1312,7 @@
     class.preorder orda (mk_less orda);
     class.preorder ordb (mk_less ordb) \<rbrakk>
   \<Longrightarrow> cont (prod_lub luba lubb) (rel_prod orda ordb) lub leq (case_prod f)"
-by(rule ccpo.cont_case_prodI)(rule Partial_Function.ccpo[OF partial_function_definitions_axioms])
+  by(rule ccpo.cont_case_prodI)(rule Partial_Function.ccpo[OF partial_function_definitions_axioms])
 
 lemma cont_case_prod_iff:
   "\<lbrakk> monotone (rel_prod orda ordb) leq (case_prod f);
@@ -1330,39 +1320,39 @@
      class.preorder ordb (mk_less ordb); lub_singleton lubb \<rbrakk>
   \<Longrightarrow> cont (prod_lub luba lubb) (rel_prod orda ordb) lub leq (case_prod f) \<longleftrightarrow>
    (\<forall>x. cont lubb ordb lub leq (\<lambda>y. f x y)) \<and> (\<forall>y. cont luba orda lub leq (\<lambda>x. f x y))"
-by(blast dest: cont_case_prodD1 cont_case_prodD2 intro: cont_case_prodI)
+  by(blast dest: cont_case_prodD1 cont_case_prodD2 intro: cont_case_prodI)
 
 lemma mcont_case_prod_iff [simp]:
   "\<lbrakk> class.preorder orda (mk_less orda); lub_singleton luba;
      class.preorder ordb (mk_less ordb); lub_singleton lubb \<rbrakk>
   \<Longrightarrow> mcont (prod_lub luba lubb) (rel_prod orda ordb) lub leq (case_prod f) \<longleftrightarrow>
    (\<forall>x. mcont lubb ordb lub leq (\<lambda>y. f x y)) \<and> (\<forall>y. mcont luba orda lub leq (\<lambda>x. f x y))"
-unfolding mcont_def by(auto simp add: cont_case_prod_iff)
+  unfolding mcont_def by(auto simp add: cont_case_prod_iff)
 
 end
 
 lemma mono2mono_case_prod [cont_intro]:
   assumes "\<And>x y. monotone orda ordb (\<lambda>f. pair f x y)"
   shows "monotone orda ordb (\<lambda>f. case_prod (pair f) x)"
-by(rule monotoneI)(auto split: prod.split dest: monotoneD[OF assms])
+  by(rule monotoneI)(auto split: prod.split dest: monotoneD[OF assms])
 
 subsection \<open>Complete lattices as ccpo\<close>
 
 context complete_lattice begin
 
 lemma complete_lattice_ccpo: "class.ccpo Sup (\<le>) (<)"
-by(unfold_locales)(fast intro: Sup_upper Sup_least)+
+  by(unfold_locales)(fast intro: Sup_upper Sup_least)+
 
 lemma complete_lattice_ccpo': "class.ccpo Sup (\<le>) (mk_less (\<le>))"
-by(unfold_locales)(auto simp add: mk_less_def intro: Sup_upper Sup_least)
+  by(unfold_locales)(auto simp add: mk_less_def intro: Sup_upper Sup_least)
 
 lemma complete_lattice_partial_function_definitions: 
   "partial_function_definitions (\<le>) Sup"
-by(unfold_locales)(auto intro: Sup_least Sup_upper)
+  by(unfold_locales)(auto intro: Sup_least Sup_upper)
 
 lemma complete_lattice_partial_function_definitions_dual:
   "partial_function_definitions (\<ge>) Inf"
-by(unfold_locales)(auto intro: Inf_lower Inf_greatest)
+  by(unfold_locales)(auto intro: Inf_lower Inf_greatest)
 
 lemmas [cont_intro, simp] =
   Partial_Function.ccpo[OF complete_lattice_partial_function_definitions]
@@ -1370,18 +1360,18 @@
 
 lemma mono2mono_inf:
   assumes f: "monotone ord (\<le>) (\<lambda>x. f x)" 
-  and g: "monotone ord (\<le>) (\<lambda>x. g x)"
+    and g: "monotone ord (\<le>) (\<lambda>x. g x)"
   shows "monotone ord (\<le>) (\<lambda>x. f x \<sqinter> g x)"
-by(auto 4 3 dest: monotoneD[OF f] monotoneD[OF g] intro: le_infI1 le_infI2 intro!: monotoneI)
+  by(auto 4 3 dest: monotoneD[OF f] monotoneD[OF g] intro: le_infI1 le_infI2 intro!: monotoneI)
 
 lemma mcont_const [simp]: "mcont lub ord Sup (\<le>) (\<lambda>_. c)"
-by(rule ccpo.mcont_const[OF complete_lattice_ccpo])
+  by(rule ccpo.mcont_const[OF complete_lattice_ccpo])
 
 lemma mono2mono_sup:
   assumes f: "monotone ord (\<le>) (\<lambda>x. f x)"
-  and g: "monotone ord (\<le>) (\<lambda>x. g x)"
+    and g: "monotone ord (\<le>) (\<lambda>x. g x)"
   shows "monotone ord (\<le>) (\<lambda>x. f x \<squnion> g x)"
-by(auto 4 3 intro!: monotoneI intro: sup.coboundedI1 sup.coboundedI2 dest: monotoneD[OF f] monotoneD[OF g])
+  by(auto 4 3 intro!: monotoneI intro: sup.coboundedI1 sup.coboundedI2 dest: monotoneD[OF f] monotoneD[OF g])
 
 lemma Sup_image_sup: 
   assumes "Y \<noteq> {}"
@@ -1408,16 +1398,16 @@
 qed
 
 lemma mcont_sup1: "mcont Sup (\<le>) Sup (\<le>) (\<lambda>y. x \<squnion> y)"
-by(auto 4 3 simp add: mcont_def sup.coboundedI1 sup.coboundedI2 intro!: monotoneI contI intro: Sup_image_sup[symmetric])
+  by(auto 4 3 simp add: mcont_def sup.coboundedI1 sup.coboundedI2 intro!: monotoneI contI intro: Sup_image_sup[symmetric])
 
 lemma mcont_sup2: "mcont Sup (\<le>) Sup (\<le>) (\<lambda>x. x \<squnion> y)"
-by(subst sup_commute)(rule mcont_sup1)
+  by(subst sup_commute)(rule mcont_sup1)
 
 lemma mcont2mcont_sup [cont_intro, simp]:
   "\<lbrakk> mcont lub ord Sup (\<le>) (\<lambda>x. f x);
      mcont lub ord Sup (\<le>) (\<lambda>x. g x) \<rbrakk>
   \<Longrightarrow> mcont lub ord Sup (\<le>) (\<lambda>x. f x \<squnion> g x)"
-by(best intro: ccpo.mcont2mcont'[OF complete_lattice_ccpo] mcont_sup1 mcont_sup2 ccpo.mcont_const[OF complete_lattice_ccpo])
+  by(best intro: ccpo.mcont2mcont'[OF complete_lattice_ccpo] mcont_sup1 mcont_sup2 ccpo.mcont_const[OF complete_lattice_ccpo])
 
 end
 
@@ -1426,59 +1416,59 @@
 context complete_distrib_lattice begin
 
 lemma mcont_inf1: "mcont Sup (\<le>) Sup (\<le>) (\<lambda>y. x \<sqinter> y)"
-by(auto intro: monotoneI contI simp add: le_infI2 inf_Sup mcont_def)
+  by(auto intro: monotoneI contI simp add: le_infI2 inf_Sup mcont_def)
 
 lemma mcont_inf2: "mcont Sup (\<le>) Sup (\<le>) (\<lambda>x. x \<sqinter> y)"
-by(auto intro: monotoneI contI simp add: le_infI1 Sup_inf mcont_def)
+  by(auto intro: monotoneI contI simp add: le_infI1 Sup_inf mcont_def)
 
 lemma mcont2mcont_inf [cont_intro, simp]:
   "\<lbrakk> mcont lub ord Sup (\<le>) (\<lambda>x. f x);
     mcont lub ord Sup (\<le>) (\<lambda>x. g x) \<rbrakk>
   \<Longrightarrow> mcont lub ord Sup (\<le>) (\<lambda>x. f x \<sqinter> g x)"
-by(best intro: ccpo.mcont2mcont'[OF complete_lattice_ccpo] mcont_inf1 mcont_inf2 ccpo.mcont_const[OF complete_lattice_ccpo])
+  by(best intro: ccpo.mcont2mcont'[OF complete_lattice_ccpo] mcont_inf1 mcont_inf2 ccpo.mcont_const[OF complete_lattice_ccpo])
 
 end
 
 interpretation lfp: partial_function_definitions "(\<le>) :: _ :: complete_lattice \<Rightarrow> _" Sup
-by(rule complete_lattice_partial_function_definitions)
+  by(rule complete_lattice_partial_function_definitions)
 
 declaration \<open>Partial_Function.init "lfp" \<^term>\<open>lfp.fixp_fun\<close> \<^term>\<open>lfp.mono_body\<close>
   @{thm lfp.fixp_rule_uc} @{thm lfp.fixp_induct_uc} NONE\<close>
 
 interpretation gfp: partial_function_definitions "(\<ge>) :: _ :: complete_lattice \<Rightarrow> _" Inf
-by(rule complete_lattice_partial_function_definitions_dual)
+  by(rule complete_lattice_partial_function_definitions_dual)
 
 declaration \<open>Partial_Function.init "gfp" \<^term>\<open>gfp.fixp_fun\<close> \<^term>\<open>gfp.mono_body\<close>
   @{thm gfp.fixp_rule_uc} @{thm gfp.fixp_induct_uc} NONE\<close>
 
 lemma insert_mono [partial_function_mono]:
-   "monotone (fun_ord (\<subseteq>)) (\<subseteq>) A \<Longrightarrow> monotone (fun_ord (\<subseteq>)) (\<subseteq>) (\<lambda>y. insert x (A y))"
-by(rule monotoneI)(auto simp add: fun_ord_def dest: monotoneD)
+  "monotone (fun_ord (\<subseteq>)) (\<subseteq>) A \<Longrightarrow> monotone (fun_ord (\<subseteq>)) (\<subseteq>) (\<lambda>y. insert x (A y))"
+  by(rule monotoneI)(auto simp add: fun_ord_def dest: monotoneD)
 
 lemma mono2mono_insert [THEN lfp.mono2mono, cont_intro, simp]:
   shows monotone_insert: "monotone (\<subseteq>) (\<subseteq>) (insert x)"
-by(rule monotoneI) blast
+  by(rule monotoneI) blast
 
 lemma mcont2mcont_insert[THEN lfp.mcont2mcont, cont_intro, simp]:
   shows mcont_insert: "mcont Union (\<subseteq>) Union (\<subseteq>) (insert x)"
-by(blast intro: mcontI contI monotone_insert)
+  by(blast intro: mcontI contI monotone_insert)
 
 lemma mono2mono_image [THEN lfp.mono2mono, cont_intro, simp]:
   shows monotone_image: "monotone (\<subseteq>) (\<subseteq>) ((`) f)"
-by(rule monotoneI) blast
+  by(rule monotoneI) blast
 
 lemma cont_image: "cont Union (\<subseteq>) Union (\<subseteq>) ((`) f)"
-by(rule contI)(auto)
+  by(rule contI)(auto)
 
 lemma mcont2mcont_image [THEN lfp.mcont2mcont, cont_intro, simp]:
   shows mcont_image: "mcont Union (\<subseteq>) Union (\<subseteq>) ((`) f)"
-by(blast intro: mcontI monotone_image cont_image)
+  by(blast intro: mcontI monotone_image cont_image)
 
 context complete_lattice begin
 
 lemma monotone_Sup [cont_intro, simp]:
   "monotone ord (\<subseteq>) f \<Longrightarrow> monotone ord (\<le>) (\<lambda>x. \<Squnion>f x)"
-by(blast intro: monotoneI Sup_least Sup_upper dest: monotoneD)
+  by(blast intro: monotoneI Sup_least Sup_upper dest: monotoneD)
 
 lemma cont_Sup:
   assumes "cont lub ord Union (\<subseteq>) f"
@@ -1694,21 +1684,21 @@
   for P
 
 lemma monotone_fst: "monotone (rel_prod orda ordb) orda fst"
-by(auto intro: monotoneI)
+  by(auto intro: monotoneI)
 
 lemma mcont_fst: "mcont (prod_lub luba lubb) (rel_prod orda ordb) luba orda fst"
-by(auto intro!: mcontI monotoneI contI simp add: prod_lub_def)
+  by(auto intro!: mcontI monotoneI contI simp add: prod_lub_def)
 
 lemma mcont2mcont_fst [cont_intro, simp]:
   "mcont lub ord (prod_lub luba lubb) (rel_prod orda ordb) t
   \<Longrightarrow> mcont lub ord luba orda (\<lambda>x. fst (t x))"
-by(auto intro!: mcontI monotoneI contI dest: mcont_monoD mcont_contD simp add: rel_prod_sel split_beta prod_lub_def image_image)
+  by(auto intro!: mcontI monotoneI contI dest: mcont_monoD mcont_contD simp add: rel_prod_sel split_beta prod_lub_def image_image)
 
 lemma monotone_snd: "monotone (rel_prod orda ordb) ordb snd"
-by(auto intro: monotoneI)
+  by(auto intro: monotoneI)
 
 lemma mcont_snd: "mcont (prod_lub luba lubb) (rel_prod orda ordb) lubb ordb snd"
-by(auto intro!: mcontI monotoneI contI simp add: prod_lub_def)
+  by(auto intro!: mcontI monotoneI contI simp add: prod_lub_def)
 
 lemma mcont2mcont_snd [cont_intro, simp]:
   "mcont lub ord (prod_lub luba lubb) (rel_prod orda ordb) t
@@ -1718,19 +1708,20 @@
 lemma monotone_Pair:
   "\<lbrakk> monotone ord orda f; monotone ord ordb g \<rbrakk>
   \<Longrightarrow> monotone ord (rel_prod orda ordb) (\<lambda>x. (f x, g x))"
-by(simp add: monotone_def)
+  by(simp add: monotone_def)
 
 lemma cont_Pair:
   "\<lbrakk> cont lub ord luba orda f; cont lub ord lubb ordb g \<rbrakk>
   \<Longrightarrow> cont lub ord (prod_lub luba lubb) (rel_prod orda ordb) (\<lambda>x. (f x, g x))"
-by(rule contI)(auto simp add: prod_lub_def image_image dest!: contD)
+  by(rule contI)(auto simp add: prod_lub_def image_image dest!: contD)
 
 lemma mcont_Pair:
   "\<lbrakk> mcont lub ord luba orda f; mcont lub ord lubb ordb g \<rbrakk>
   \<Longrightarrow> mcont lub ord (prod_lub luba lubb) (rel_prod orda ordb) (\<lambda>x. (f x, g x))"
-by(rule mcontI)(simp_all add: monotone_Pair mcont_mono cont_Pair)
+  by(rule mcontI)(simp_all add: monotone_Pair mcont_mono cont_Pair)
 
-context partial_function_definitions begin
+context partial_function_definitions 
+begin
 text \<open>Specialised versions of @{thm [source] mcont_call} for admissibility proofs for parallel fixpoint inductions\<close>
 lemmas mcont_call_fst [cont_intro] = mcont_call[THEN mcont2mcont, OF mcont_fst]
 lemmas mcont_call_snd [cont_intro] = mcont_call[THEN mcont2mcont, OF mcont_snd]
--- a/src/HOL/Library/Extended_Nat.thy	Fri Jan 17 20:30:01 2025 +0100
+++ b/src/HOL/Library/Extended_Nat.thy	Fri Jan 17 21:30:08 2025 +0100
@@ -191,10 +191,10 @@
   by (simp_all add: eSuc_plus_1 ac_simps)
 
 lemma iadd_Suc: "eSuc m + n = eSuc (m + n)"
-  by (simp_all add: eSuc_plus_1 ac_simps)
+  by (simp add: eSuc_plus_1 ac_simps)
 
 lemma iadd_Suc_right: "m + eSuc n = eSuc (m + n)"
-  by (simp only: add.commute[of m] iadd_Suc)
+  by (metis add.commute iadd_Suc)
 
 subsection \<open>Multiplication\<close>
 
@@ -216,29 +216,12 @@
 instance
 proof
   fix a b c :: enat
-  show "(a * b) * c = a * (b * c)"
-    unfolding times_enat_def zero_enat_def
-    by (simp split: enat.split)
-  show comm: "a * b = b * a"
-    unfolding times_enat_def zero_enat_def
-    by (simp split: enat.split)
-  show "1 * a = a"
-    unfolding times_enat_def zero_enat_def one_enat_def
-    by (simp split: enat.split)
   show distr: "(a + b) * c = a * c + b * c"
     unfolding times_enat_def zero_enat_def
     by (simp split: enat.split add: distrib_right)
-  show "0 * a = 0"
-    unfolding times_enat_def zero_enat_def
-    by (simp split: enat.split)
-  show "a * 0 = 0"
-    unfolding times_enat_def zero_enat_def
-    by (simp split: enat.split)
   show "a * (b + c) = a * b + a * c"
     by (cases a b c rule: enat3_cases) (auto simp: times_enat_def zero_enat_def distrib_left)
-  show "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
-    by (cases a b rule: enat2_cases) (auto simp: times_enat_def zero_enat_def)
-qed
+qed (auto simp: times_enat_def zero_enat_def one_enat_def split: enat.split)
 
 end
 
@@ -246,13 +229,10 @@
   unfolding eSuc_plus_1 by (simp add: algebra_simps)
 
 lemma mult_eSuc_right: "m * eSuc n = m + m * n"
-  unfolding eSuc_plus_1 by (simp add: algebra_simps)
+  by (metis mult.commute mult_eSuc)
 
 lemma of_nat_eq_enat: "of_nat n = enat n"
-  apply (induct n)
-  apply (simp add: enat_0)
-  apply (simp add: plus_1_eSuc eSuc_enat)
-  done
+  by (induct n) (auto simp: enat_0 plus_1_eSuc eSuc_enat)
 
 instance enat :: semiring_char_0
 proof
@@ -267,7 +247,7 @@
 
 lemma numeral_eq_enat:
   "numeral k = enat (numeral k)"
-  using of_nat_eq_enat [of "numeral k"] by simp
+  by (metis of_nat_eq_enat of_nat_numeral)
 
 lemma enat_numeral [code_abbrev]:
   "enat (numeral k) = numeral k"
@@ -349,11 +329,11 @@
 
 lemma numeral_le_enat_iff[simp]:
   shows "numeral m \<le> enat n \<longleftrightarrow> numeral m \<le> n"
-by (auto simp: numeral_eq_enat)
+  by (auto simp: numeral_eq_enat)
 
 lemma numeral_less_enat_iff[simp]:
   shows "numeral m < enat n \<longleftrightarrow> numeral m < n"
-by (auto simp: numeral_eq_enat)
+  by (auto simp: numeral_eq_enat)
 
 lemma enat_ord_code [code]:
   "enat m \<le> enat n \<longleftrightarrow> m \<le> n"
@@ -472,17 +452,15 @@
 by(cases x y rule: enat.exhaust[case_product enat.exhaust]) simp_all
 
 lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j \<Longrightarrow> \<exists>j. enat k < Y j"
-apply (induct_tac k)
- apply (simp (no_asm) only: enat_0)
- apply (fast intro: le_less_trans [OF zero_le])
-apply (erule exE)
-apply (drule spec)
-apply (erule exE)
-apply (drule ileI1)
-apply (rule eSuc_enat [THEN subst])
-apply (rule exI)
-apply (erule (1) le_less_trans)
-done
+proof (induction k)
+  case 0
+  then show ?case
+    using enat_0 zero_less_iff_neq_zero by fastforce 
+next
+  case (Suc k)
+  then show ?case
+    by (meson Suc_ile_eq order_le_less_trans)
+qed
 
 lemma eSuc_max: "eSuc (max x y) = max (eSuc x) (eSuc y)"
   by (simp add: eSuc_def split: enat.split)
@@ -490,10 +468,7 @@
 lemma eSuc_Max:
   assumes "finite A" "A \<noteq> {}"
   shows "eSuc (Max A) = Max (eSuc ` A)"
-using assms proof induction
-  case (insert x A)
-  thus ?case by(cases "A = {}")(simp_all add: eSuc_max)
-qed simp
+  by (simp add: assms mono_Max_commute mono_eSuc)
 
 instantiation enat :: "{order_bot, order_top}"
 begin
@@ -511,19 +486,16 @@
   shows "finite A"
 proof (rule finite_subset)
   show "finite (enat ` {..n})" by blast
-  have "A \<subseteq> {..enat n}" using le_fin by fastforce
-  also have "\<dots> \<subseteq> enat ` {..n}"
-    apply (rule subsetI)
-    subgoal for x by (cases x) auto
-    done
-  finally show "A \<subseteq> enat ` {..n}" .
+  have "A \<subseteq> enat ` {..n}"
+    using enat_ile le_fin by fastforce
+  then show "A \<subseteq> enat ` {..n}" .
 qed
 
 
 subsection \<open>Cancellation simprocs\<close>
 
 lemma add_diff_cancel_enat[simp]: "x \<noteq> \<infinity> \<Longrightarrow> x + y - x = (y::enat)"
-by (metis add.commute add.right_neutral add_diff_assoc_enat idiff_self order_refl)
+  by (metis add.commute add.right_neutral add_diff_assoc_enat idiff_self order_refl)
 
 lemma enat_add_left_cancel: "a + b = a + c \<longleftrightarrow> a = (\<infinity>::enat) \<or> b = c"
   unfolding plus_enat_def by (simp split: enat.split)
@@ -535,7 +507,7 @@
   unfolding plus_enat_def by (simp split: enat.split)
 
 lemma plus_eq_infty_iff_enat: "(m::enat) + n = \<infinity> \<longleftrightarrow> m=\<infinity> \<or> n=\<infinity>"
-using enat_add_left_cancel by fastforce
+  using enat_add_left_cancel by fastforce
 
 ML \<open>
 structure Cancel_Enat_Common =
@@ -605,32 +577,21 @@
 subsection \<open>Well-ordering\<close>
 
 lemma less_enatE:
-  "[| n < enat m; !!k. n = enat k ==> k < m ==> P |] ==> P"
-by (induct n) auto
+  "\<lbrakk>n < enat m; \<And>k. \<lbrakk>n = enat k; k < m\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
+  using enat_iless enat_ord_simps(2) by blast
 
 lemma less_infinityE:
-  "[| n < \<infinity>; !!k. n = enat k ==> P |] ==> P"
-by (induct n) auto
+  "\<lbrakk>n < \<infinity>; \<And>k. n = enat k \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
+  by auto
 
 lemma enat_less_induct:
-  assumes prem: "\<And>n. \<forall>m::enat. m < n \<longrightarrow> P m \<Longrightarrow> P n" shows "P n"
+  assumes "\<And>n. \<forall>m::enat. m < n \<longrightarrow> P m \<Longrightarrow> P n" 
+  shows "P n"
 proof -
-  have P_enat: "\<And>k. P (enat k)"
-    apply (rule nat_less_induct)
-    apply (rule prem, clarify)
-    apply (erule less_enatE, simp)
-    done
-  show ?thesis
-  proof (induct n)
-    fix nat
-    show "P (enat nat)" by (rule P_enat)
-  next
-    show "P \<infinity>"
-      apply (rule prem, clarify)
-      apply (erule less_infinityE)
-      apply (simp add: P_enat)
-      done
-  qed
+  have "P (enat k)" for k
+    by (induction k rule: less_induct) (metis less_enatE assms)
+  then show ?thesis
+    by (metis enat.exhaust less_infinityE assms)
 qed
 
 instance enat :: wellorder
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Fri Jan 17 20:30:01 2025 +0100
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Fri Jan 17 21:30:08 2025 +0100
@@ -16,20 +16,17 @@
 lemma Limsup_const_add:
   fixes c :: "'a::{complete_linorder, linorder_topology, topological_monoid_add, ordered_ab_semigroup_add}"
   shows "F \<noteq> bot \<Longrightarrow> Limsup F (\<lambda>x. c + f x) = c + Limsup F f"
-  by (rule Limsup_compose_continuous_mono)
-     (auto intro!: monoI add_mono continuous_on_add continuous_on_id continuous_on_const)
+  by (intro Limsup_compose_continuous_mono monoI add_mono continuous_intros) auto
 
 lemma Liminf_const_add:
   fixes c :: "'a::{complete_linorder, linorder_topology, topological_monoid_add, ordered_ab_semigroup_add}"
   shows "F \<noteq> bot \<Longrightarrow> Liminf F (\<lambda>x. c + f x) = c + Liminf F f"
-  by (rule Liminf_compose_continuous_mono)
-     (auto intro!: monoI add_mono continuous_on_add continuous_on_id continuous_on_const)
+  by (intro Liminf_compose_continuous_mono monoI add_mono continuous_intros) auto
 
 lemma Liminf_add_const:
   fixes c :: "'a::{complete_linorder, linorder_topology, topological_monoid_add, ordered_ab_semigroup_add}"
   shows "F \<noteq> bot \<Longrightarrow> Liminf F (\<lambda>x. f x + c) = Liminf F f + c"
-  by (rule Liminf_compose_continuous_mono)
-     (auto intro!: monoI add_mono continuous_on_add continuous_on_id continuous_on_const)
+  by (intro Liminf_compose_continuous_mono monoI add_mono continuous_intros) auto
 
 lemma sums_offset:
   fixes f g :: "nat \<Rightarrow> 'a :: {t2_space, topological_comm_monoid_add}"
@@ -96,9 +93,7 @@
     by (induction i) (auto simp: bot eq f_le_lfp intro!: le_lfp mg)
   then show "\<alpha> (lfp f) \<le> lfp g"
     unfolding sup_continuous_lfp[OF f]
-    by (subst \<alpha>[THEN sup_continuousD])
-       (auto intro!: mono_funpow sup_continuous_mono[OF f] SUP_least)
-
+    by (simp add: SUP_least \<alpha>[THEN sup_continuousD] mf mono_funpow)
   show "lfp g \<le> \<alpha> (lfp f)"
     by (rule lfp_lowerbound) (simp add: eq[symmetric] lfp_fixpoint[OF mf])
 qed
@@ -337,16 +332,17 @@
 
 lemma rel_fun_limsup[transfer_rule]: "rel_fun (rel_fun (=) pcr_ennreal) pcr_ennreal limsup limsup"
 proof -
+  have [simp]: "max 0 (SUP x\<in>{n..}. enn2ereal (y x)) = (SUP x\<in>{n..}. enn2ereal (y x))" for n::nat and y
+    by (meson SUP_upper atLeast_iff enn2ereal_nonneg max.absorb2 nle_le order_trans)
   have "rel_fun (rel_fun (=) pcr_ennreal) pcr_ennreal (\<lambda>x. INF n. sup 0 (SUP i\<in>{n..}. x i)) limsup"
     unfolding limsup_INF_SUP[abs_def] by (transfer_prover_start, transfer_step+; simp)
-  then show ?thesis
-    unfolding limsup_INF_SUP[abs_def]
-    apply (subst (asm) (2) rel_fun_def)
-    apply (subst (2) rel_fun_def)
-    apply (auto simp: comp_def max.absorb2 Sup_upper2 rel_fun_eq_pcr_ennreal)
-    apply (subst (asm) max.absorb2)
-    apply (auto intro: SUP_upper2)
-    done
+  moreover 
+  have "\<And>x y. \<lbrakk>rel_fun (=) pcr_ennreal x y;
+                pcr_ennreal (INF n::nat. max 0 (Sup (x ` {n..}))) (INF n. Sup (y ` {n..}))\<rbrakk>
+           \<Longrightarrow> pcr_ennreal (INF n. Sup (x ` {n..})) (INF n. Sup (y ` {n..}))"
+    by (auto simp: comp_def rel_fun_eq_pcr_ennreal)
+  ultimately show ?thesis
+    by (simp add: limsup_INF_SUP rel_fun_def)
 qed
 
 lemma sum_enn2ereal[simp]: "(\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> (\<Sum>i\<in>I. enn2ereal (f i)) = enn2ereal (sum f I)"
@@ -363,7 +359,7 @@
   by (metis enn2ereal_of_nat numeral_eq_ereal of_nat_numeral)
 
 lemma transfer_numeral[transfer_rule]: "pcr_ennreal (numeral a) (numeral a)"
-  unfolding cr_ennreal_def pcr_ennreal_def by auto
+  by (metis enn2ereal_numeral pcr_ennreal_enn2ereal)
 
 subsection \<open>Cancellation simprocs\<close>
 
@@ -654,7 +650,7 @@
   fixes a b c :: ennreal
   shows "a - b \<le> a - c \<Longrightarrow> a < top \<Longrightarrow> b \<le> a \<Longrightarrow> c \<le> a \<Longrightarrow> c \<le> b"
   by transfer
-     (auto simp add: max.absorb2 ereal_diff_positive top_ereal_def dest: ereal_mono_minus_cancel)
+     (auto simp add: ereal_diff_positive top_ereal_def dest: ereal_mono_minus_cancel)
 
 lemma ennreal_mono_minus:
   fixes a b c :: ennreal
@@ -718,16 +714,13 @@
   done
 
 lemma ennreal_inverse_mult: "a < top \<Longrightarrow> b < top \<Longrightarrow> inverse (a * b::ennreal) = inverse a * inverse b"
-  apply transfer
-  subgoal for a b
-    by (cases a b rule: ereal2_cases) (auto simp: top_ereal_def)
-  done
+  by (simp add: ennreal_inverse_mult')
 
 lemma ennreal_inverse_1[simp]: "inverse (1::ennreal) = 1"
   by transfer simp
 
 lemma ennreal_inverse_eq_0_iff[simp]: "inverse (a::ennreal) = 0 \<longleftrightarrow> a = top"
-  by transfer (simp add: ereal_inverse_eq_0 top_ereal_def)
+  by (metis ennreal_inverse_positive not_gr_zero)
 
 lemma ennreal_inverse_eq_top_iff[simp]: "inverse (a::ennreal) = top \<longleftrightarrow> a = 0"
   by transfer (simp add: top_ereal_def)
@@ -752,7 +745,7 @@
   by (cases "a = 0") simp_all
 
 lemma ennreal_zero_less_mult_iff: "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < (b::ennreal)"
-  by transfer (auto simp add: ereal_zero_less_0_iff le_less)
+  using not_gr_zero by fastforce
 
 lemma less_diff_eq_ennreal:
   fixes a b c :: ennreal
@@ -768,7 +761,7 @@
   by transfer (metis (no_types) add.commute ereal_diff_positive ereal_ineq_diff_add max_def not_MInfty_nonneg)
 
 lemma ennreal_diff_self[simp]: "a \<noteq> top \<Longrightarrow> a - a = (0::ennreal)"
-  by transfer (simp add: top_ereal_def)
+  by (meson ennreal_minus_pos_iff less_imp_neq not_gr_zero top.not_eq_extremum)
 
 lemma ennreal_minus_mono:
   fixes a b c :: ennreal
@@ -852,7 +845,7 @@
 by (metis e2ennreal_def enn2ereal_inverse ennreal.rep_eq sup_ereal_def)
 
 lemma ennreal_0[simp]: "ennreal 0 = 0"
-  by (simp add: ennreal_def max.absorb1 zero_ennreal.abs_eq)
+  by (simp add: ennreal_def zero_ennreal.abs_eq)
 
 lemma ennreal_1[simp]: "ennreal 1 = 1"
   by transfer (simp add: max_absorb2)
@@ -926,11 +919,10 @@
   by (auto split: split_min)
 
 lemma ennreal_half[simp]: "ennreal (1/2) = inverse 2"
-  by transfer (simp add: max.absorb2)
+  by transfer auto
 
 lemma ennreal_minus: "0 \<le> q \<Longrightarrow> ennreal r - ennreal q = ennreal (r - q)"
-  by transfer
-     (simp add: max.absorb2 zero_ereal_def flip: ereal_max)
+  by transfer (simp add: zero_ereal_def flip: ereal_max)
 
 lemma ennreal_minus_top[simp]: "ennreal a - top = 0"
   by (simp add: minus_top_ennreal)
@@ -958,8 +950,7 @@
   by (induction n) (auto simp: ennreal_mult)
 
 lemma power_eq_top_ennreal: "x ^ n = top \<longleftrightarrow> (n \<noteq> 0 \<and> (x::ennreal) = top)"
-  by (cases x rule: ennreal_cases)
-     (auto simp: ennreal_power top_power_ennreal)
+  using not_gr_zero power_eq_top_ennreal_iff by force
 
 lemma inverse_ennreal: "0 < r \<Longrightarrow> inverse (ennreal r) = ennreal (inverse r)"
   by transfer (simp add: max.absorb2)
@@ -982,7 +973,7 @@
 
 lemma power_divide_distrib_ennreal [algebra_simps]:
   "(x / y) ^ n = x ^ n / (y ^ n :: ennreal)"
-  by (simp add: divide_ennreal_def algebra_simps ennreal_inverse_power)
+  by (simp add: divide_ennreal_def ennreal_inverse_power power_mult_distrib)
 
 lemma ennreal_divide_numeral: "0 \<le> x \<Longrightarrow> ennreal x / numeral b = ennreal (x / numeral b)"
   by (subst divide_ennreal[symmetric]) auto
@@ -997,11 +988,7 @@
   using assms by (induction A rule: infinite_finite_induct) (auto intro!: mult_mono)
 
 lemma mult_right_ennreal_cancel: "a * ennreal c = b * ennreal c \<longleftrightarrow> (a = b \<or> c \<le> 0)"
-proof (cases "0 \<le> c")
-  case True
-  then show ?thesis
-    by (metis ennreal_eq_0_iff ennreal_mult_right_cong ennreal_neq_top mult_divide_eq_ennreal)
-qed (use ennreal_neg in auto)
+  by (metis ennreal_eq_0_iff mult_divide_eq_ennreal mult_eq_0_iff top_neq_ennreal)
 
 lemma ennreal_le_epsilon:
   "(\<And>e::real. y < top \<Longrightarrow> 0 < e \<Longrightarrow> x \<le> y + ennreal e) \<Longrightarrow> x \<le> y"
@@ -1166,13 +1153,13 @@
 lemma enn2ereal_Iio: "enn2ereal -` {..<a} = (if 0 \<le> a then {..< e2ennreal a} else {})"
   using enn2ereal_nonneg
   by (cases a rule: ereal_ennreal_cases)
-     (auto simp add: vimage_def set_eq_iff ennreal.enn2ereal_inverse less_ennreal.rep_eq e2ennreal_def max_absorb2
+     (auto simp add: vimage_def set_eq_iff ennreal.enn2ereal_inverse less_ennreal.rep_eq e2ennreal_def 
            simp del: enn2ereal_nonneg
            intro: le_less_trans less_imp_le)
 
 lemma enn2ereal_Ioi: "enn2ereal -` {a <..} = (if 0 \<le> a then {e2ennreal a <..} else UNIV)"
   by (cases a rule: ereal_ennreal_cases)
-     (auto simp add: vimage_def set_eq_iff ennreal.enn2ereal_inverse less_ennreal.rep_eq e2ennreal_def max_absorb2
+     (auto simp add: vimage_def set_eq_iff ennreal.enn2ereal_inverse less_ennreal.rep_eq e2ennreal_def 
            intro: less_le_trans)
 
 instantiation ennreal :: linear_continuum_topology
@@ -1203,25 +1190,23 @@
   show "continuous_on ({0..} \<union> {..0}) e2ennreal"
   proof (rule continuous_on_closed_Un)
     show "continuous_on {0 ..} e2ennreal"
-      by (rule continuous_onI_mono)
-         (auto simp add: less_eq_ennreal.abs_eq eq_onp_def enn2ereal_range)
+      by (simp add: continuous_onI_mono e2ennreal_mono enn2ereal_range)
     show "continuous_on {.. 0} e2ennreal"
-      by (subst continuous_on_cong[OF refl, of _ _ "\<lambda>_. 0"])
-         (auto simp add: e2ennreal_neg continuous_on_const)
+      by (metis atMost_iff continuous_on_cong continuous_on_const e2ennreal_neg)
   qed auto
-  show "A \<subseteq> {0..} \<union> {..0::ereal}"
-    by auto
-qed
+qed auto
 
 lemma continuous_at_e2ennreal: "continuous (at x within A) e2ennreal"
-  by (rule continuous_on_imp_continuous_within[OF continuous_on_e2ennreal, of _ UNIV]) auto
+  using continuous_on_e2ennreal continuous_on_imp_continuous_within top.extremum
+  by blast
 
 lemma continuous_on_enn2ereal: "continuous_on UNIV enn2ereal"
   by (rule continuous_on_generate_topology[OF open_generated_order])
      (auto simp add: enn2ereal_Iio enn2ereal_Ioi)
 
 lemma continuous_at_enn2ereal: "continuous (at x within A) enn2ereal"
-  by (rule continuous_on_imp_continuous_within[OF continuous_on_enn2ereal]) auto
+  by (meson UNIV_I continuous_at_imp_continuous_at_within
+      continuous_on_enn2ereal continuous_on_eq_continuous_within)
 
 lemma sup_continuous_e2ennreal[order_continuous_intros]:
   assumes f: "sup_continuous f" shows "sup_continuous (\<lambda>x. e2ennreal (f x))"
@@ -1370,7 +1355,7 @@
   unfolding sums_def by (simp add: always_eventually sum_nonneg)
 
 lemma suminf_enn2ereal[simp]: "(\<Sum>i. enn2ereal (f i)) = enn2ereal (suminf f)"
-  by (rule sums_unique[symmetric]) (simp add: summable_sums)
+  by (metis summableI summable_sums sums_enn2ereal sums_unique)
 
 lemma transfer_e2ennreal_suminf [transfer_rule]: "rel_fun (rel_fun (=) pcr_ennreal) pcr_ennreal suminf suminf"
   by (auto simp: rel_funI rel_fun_eq_pcr_ennreal comp_def)
@@ -1565,7 +1550,7 @@
   fixes f g :: "nat \<Rightarrow> ennreal"
   shows "(\<And>i. g i \<le> f i) \<Longrightarrow> suminf f \<noteq> top \<Longrightarrow> suminf g \<noteq> top \<Longrightarrow> (\<Sum>i. f i - g i) = suminf f - suminf g"
   by transfer
-     (auto simp add: max.absorb2 ereal_diff_positive suminf_le_pos top_ereal_def intro!: suminf_ereal_minus)
+     (auto simp add: ereal_diff_positive suminf_le_pos top_ereal_def intro!: suminf_ereal_minus)
 
 lemma ennreal_Sup_countable_SUP:
   "A \<noteq> {} \<Longrightarrow> \<exists>f::nat \<Rightarrow> ennreal. incseq f \<and> range f \<subseteq> A \<and> Sup A = (SUP i. f i)"
@@ -1605,7 +1590,7 @@
   have "f (SUP i \<in> I. g i) = (SUP i \<in> range M. f i)"
     unfolding eq sup_continuousD[OF f \<open>mono M\<close>] by (simp add: image_comp)
   also have "\<dots> \<le> (SUP i \<in> I. f (g i))"
-    by (insert M, drule SUP_subset_mono) (auto simp add: image_comp)
+    by (smt (verit) M SUP_le_iff dual_order.refl image_iff subsetD)
   finally show "f (SUP i \<in> I. g i) \<le> (SUP i \<in> I. f (g i))" .
 qed
 
@@ -1633,8 +1618,9 @@
 
 (* Contributed by Dominique Unruh *)
 lemma isCont_ennreal[simp]: \<open>isCont ennreal x\<close>
-  apply (auto intro!: sequentially_imp_eventually_within simp: continuous_within tendsto_def)
-  by (metis tendsto_def tendsto_ennrealI)
+  unfolding continuous_within tendsto_def
+  using tendsto_ennrealI topological_tendstoD  
+  by (blast intro: sequentially_imp_eventually_within)
 
 (* Contributed by Dominique Unruh *)
 lemma isCont_ennreal_of_enat[simp]: \<open>isCont ennreal_of_enat x\<close>
@@ -1672,12 +1658,8 @@
     define s where \<open>s = {x}\<close>
     have \<open>open s\<close>
       using False open_enat_iff s_def by blast
-    moreover have \<open>x \<in> s\<close>
-      using s_def by auto
-    moreover have \<open>ennreal_of_enat z \<in> t\<close> if \<open>z \<in> s\<close> for z
-      using asm s_def that by blast
-    ultimately show \<open>\<exists>s. open s \<and> x \<in> s \<and> (\<forall>z\<in>s. ennreal_of_enat z \<in> t)\<close>
-      by auto
+    then show \<open>\<exists>s. open s \<and> x \<in> s \<and> (\<forall>z\<in>s. ennreal_of_enat z \<in> t)\<close>
+      using asm s_def by blast
   qed
 qed
 
@@ -1686,15 +1668,10 @@
 lemma INF_approx_ennreal:
   fixes x::ennreal and e::real
   assumes "e > 0"
-  assumes INF: "x = (INF i \<in> A. f i)"
+  assumes "x = (INF i \<in> A. f i)"
   assumes "x \<noteq> \<infinity>"
   shows "\<exists>i \<in> A. f i < x + e"
-proof -
-  have "(INF i \<in> A. f i) < x + e"
-    unfolding INF[symmetric] using \<open>0<e\<close> \<open>x \<noteq> \<infinity>\<close> by (cases x) auto
-  then show ?thesis
-    unfolding INF_less_iff .
-qed
+  using INF_less_iff assms by fastforce
 
 lemma SUP_approx_ennreal:
   fixes x::ennreal and e::real
@@ -1751,9 +1728,9 @@
 
 lemma ennreal_approx_unit:
   "(\<And>a::ennreal. 0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a * z \<le> y) \<Longrightarrow> z \<le> y"
-  apply (subst SUP_mult_right_ennreal[of "\<lambda>x. x" "{0 <..< 1}" z, simplified])
-  apply (auto intro: SUP_least)
-  done
+  using SUP_mult_right_ennreal[of "\<lambda>x. x" "{0 <..< 1}" z]
+  by (smt (verit) SUP_least Sup_greaterThanLessThan greaterThanLessThan_iff
+      image_ident mult_1 zero_less_one)
 
 lemma suminf_ennreal2:
   "(\<And>i. 0 \<le> f i) \<Longrightarrow> summable f \<Longrightarrow> (\<Sum>i. ennreal (f i)) = ennreal (\<Sum>i. f i)"
@@ -1784,11 +1761,8 @@
 lemma ennreal_tendsto_top_eq_at_top:
   "((\<lambda>z. ennreal (f z)) \<longlongrightarrow> top) F \<longleftrightarrow> (LIM z F. f z :> at_top)"
   unfolding filterlim_at_top_dense tendsto_top_iff_ennreal
-  using ennreal_less_iff eventually_mono
-  apply (auto simp: ennreal_less_iff)
-  subgoal for y
-    by (auto elim!: eventually_mono allE[of _ "max 0 y"])
-  done
+  using ennreal_less_iff eventually_mono allE[of _ "max 0 _"]
+  by (smt (verit) linorder_not_less order_refl order_trans)
 
 lemma tendsto_0_if_Limsup_eq_0_ennreal:
   fixes f :: "_ \<Rightarrow> ennreal"
@@ -1874,10 +1848,7 @@
 
 lemma add_diff_eq_iff_ennreal[simp]:
   fixes x y :: ennreal shows "x + (y - x) = y \<longleftrightarrow> x \<le> y"
-proof
-  assume *: "x + (y - x) = y" show "x \<le> y"
-    by (subst *[symmetric]) simp
-qed (simp add: add_diff_inverse_ennreal)
+  by (metis ennreal_ineq_diff_add le_iff_add)
 
 lemma add_diff_le_ennreal: "a + b - c \<le> a + (b - c::ennreal)"
   apply (cases a b c rule: ennreal3_cases)
@@ -1901,7 +1872,8 @@
            simp flip: ennreal_plus)
 
 lemma power_less_top_ennreal: fixes x :: ennreal shows "x ^ n < top \<longleftrightarrow> x < top \<or> n = 0"
-  using power_eq_top_ennreal[of x n] by (auto simp: less_top)
+  using power_eq_top_ennreal top.not_eq_extremum
+  by blast
 
 lemma ennreal_divide_times: "(a / b) * c = a * (c / b :: ennreal)"
   by (simp add: mult.commute ennreal_times_divide)
@@ -1914,7 +1886,7 @@
      (auto simp: divide_ennreal ennreal_mult[symmetric] ennreal_less_iff field_simps ennreal_top_mult ennreal_top_divide)
 
 lemma one_less_numeral[simp]: "1 < (numeral n::ennreal) \<longleftrightarrow> (num.One < n)"
-  by (simp flip: ennreal_1 ennreal_numeral add: ennreal_less_iff)
+  by simp
 
 lemma divide_eq_1_ennreal: "a / b = (1::ennreal) \<longleftrightarrow> (b \<noteq> top \<and> b \<noteq> 0 \<and> b = a)"
   by (cases a ; cases b; cases "b = 0") (auto simp: ennreal_top_divide divide_ennreal split: if_split_asm)
--- a/src/HOL/Library/Float.thy	Fri Jan 17 20:30:01 2025 +0100
+++ b/src/HOL/Library/Float.thy	Fri Jan 17 21:30:08 2025 +0100
@@ -113,7 +113,7 @@
   by (cases x rule: linorder_cases[of 0]) auto
 
 lemma sgn_of_float[simp]: "x \<in> float \<Longrightarrow> sgn x \<in> float"
-  by (cases x rule: linorder_cases[of 0]) (auto intro!: uminus_float)
+  by (simp add: sgn_real_def)
 
 lemma div_power_2_float[simp]: "x \<in> float \<Longrightarrow> x / 2^d \<in> float" 
   by (simp add: float_def) (metis of_int_diff of_int_of_nat_eq powr_diff powr_realpow zero_less_numeral times_divide_eq_right)
@@ -144,8 +144,8 @@
   from assms obtain m e :: int where "a = m * 2 powr e"
     by (auto simp: float_def)
   then show ?thesis
-    by (auto intro!: floatI[where m="m^b" and e = "e*b"]
-      simp: power_mult_distrib powr_realpow[symmetric] powr_powr)
+    by (intro floatI[where m="m^b" and e = "e*b"])
+       (auto simp: powr_powr power_mult_distrib simp flip: powr_realpow)
 qed
 
 lift_definition Float :: "int \<Rightarrow> int \<Rightarrow> float" is "\<lambda>(m::int) (e::int). m * 2 powr e"
@@ -383,11 +383,10 @@
       by (auto simp: float_def)
     with \<open>x \<noteq> 0\<close> int_cancel_factors[of 2 m] obtain k i where "m = k * 2 ^ i" "\<not> 2 dvd k"
       by auto
-    with \<open>\<not> 2 dvd k\<close> x show ?thesis
-      apply (rule_tac exI[of _ "k"])
-      apply (rule_tac exI[of _ "e + int i"])
-      apply (simp add: powr_add powr_realpow)
-      done
+    with \<open>\<not> 2 dvd k\<close> x have "x = real_of_int k * 2 powr real_of_int (e + int i) \<and> odd k"
+      by (simp add: powr_add powr_realpow)
+    then show ?thesis
+      by blast
   qed
   with that show thesis by blast
 qed
@@ -799,7 +798,7 @@
     apply (metis (no_types, opaque_lifting) Float.rep_eq
       add.inverse_inverse compute_real_of_float diff_minus_eq_add
       floor_divide_of_int_eq int_of_reals(1) linorder_not_le
-      minus_add_distrib of_int_eq_numeral_power_cancel_iff )
+      minus_add_distrib of_int_eq_numeral_power_cancel_iff)
     done
 next
   case False
@@ -1190,7 +1189,7 @@
         using logless flogless \<open>x > 0\<close> \<open>y > 0\<close>
         by (auto intro!: floor_mono)
       finally show ?thesis
-        by (auto simp flip: powr_realpow simp: powr_diff assms of_nat_diff)
+        by (auto simp flip: powr_realpow simp: powr_diff assms)
     qed
     ultimately show ?thesis
       by (metis dual_order.trans truncate_down)
@@ -1264,11 +1263,9 @@
   note powr_strict = powr_less_cancel_iff[symmetric, OF \<open>1 < p\<close>, THEN iffD2]
   have "floor ?r = (if i \<ge> j * p powr (?fl i - ?fl j) then 0 else -1)" (is "_ = ?if")
     using assms
-    by (linarith |
-      auto
-        intro!: floor_eq2
-        intro: powr_strict powr
-        simp: powr_diff powr_add field_split_simps algebra_simps)+
+    apply simp
+    by (smt (verit, ccfv_SIG) floor_less_iff floor_uminus_of_int le_log_iff mult_powr_eq
+        of_int_1 real_of_int_floor_add_one_gt zero_le_floor)
   finally
   show ?thesis by simp
 qed
@@ -1852,7 +1849,7 @@
            (plus_down prec (nprt b * nprt bb)
              (plus_down prec (pprt a * pprt ab)
                (pprt b * nprt ab)))"
-  by (smt (verit, del_insts) mult_mono plus_down_mono add_mono nprt_mono nprt_le_zero zero_le_pprt 
+  by (smt (verit, best) mult_mono plus_down_mono add_mono nprt_mono nprt_le_zero zero_le_pprt 
 pprt_mono mult_mono_nonpos_nonneg mult_mono_nonpos_nonpos mult_mono_nonneg_nonpos)
 
 lemma mult_float_mono2:
@@ -1870,7 +1867,7 @@
            (plus_up prec (pprt aa * nprt bc)
              (plus_up prec (nprt ba * pprt ac)
                (nprt aa * nprt ac)))"
-  by (smt (verit, del_insts) plus_up_mono add_mono mult_mono nprt_mono nprt_le_zero zero_le_pprt pprt_mono 
+  by (smt (verit, best) plus_up_mono add_mono mult_mono nprt_mono nprt_le_zero zero_le_pprt pprt_mono 
       mult_mono_nonpos_nonneg mult_mono_nonpos_nonpos mult_mono_nonneg_nonpos)
 
 
@@ -2164,7 +2161,7 @@
   by transfer (simp add: truncate_down_nonneg)
 
 lemma rapprox_rat: "real_of_int x / real_of_int y \<le> real_of_float (rapprox_rat prec x y)"
-  by transfer (simp add: truncate_up)
+  by (simp add: rapprox_rat.rep_eq truncate_up)
 
 lemma rapprox_rat_le1:
   assumes "0 \<le> x" "0 < y" "x \<le> y"
@@ -2232,7 +2229,7 @@
   by transfer (rule real_divl_pos_less1_bound)
 
 lemma float_divr: "real_of_float x / real_of_float y \<le> real_of_float (float_divr prec x y)"
-  by transfer (rule real_divr)
+  by (simp add: float_divr.rep_eq real_divr)
 
 lemma real_divr_pos_less1_lower_bound:
   assumes "0 < x"
--- a/src/HOL/Library/ListVector.thy	Fri Jan 17 20:30:01 2025 +0100
+++ b/src/HOL/Library/ListVector.thy	Fri Jan 17 21:30:08 2025 +0100
@@ -3,7 +3,7 @@
 section \<open>Lists as vectors\<close>
 
 theory ListVector
-imports Main
+  imports Main
 begin
 
 text\<open>\noindent
@@ -13,19 +13,19 @@
 text\<open>Multiplication with a scalar:\<close>
 
 abbreviation scale :: "('a::times) \<Rightarrow> 'a list \<Rightarrow> 'a list" (infix \<open>*\<^sub>s\<close> 70)
-where "x *\<^sub>s xs \<equiv> map ((*) x) xs"
+  where "x *\<^sub>s xs \<equiv> map ((*) x) xs"
 
 lemma scale1[simp]: "(1::'a::monoid_mult) *\<^sub>s xs = xs"
-by (induct xs) simp_all
+  by (induct xs) simp_all
 
 subsection \<open>\<open>+\<close> and \<open>-\<close>\<close>
 
 fun zipwith0 :: "('a::zero \<Rightarrow> 'b::zero \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
-where
-"zipwith0 f [] [] = []" |
-"zipwith0 f (x#xs) (y#ys) = f x y # zipwith0 f xs ys" |
-"zipwith0 f (x#xs) [] = f x 0 # zipwith0 f xs []" |
-"zipwith0 f [] (y#ys) = f 0 y # zipwith0 f [] ys"
+  where
+    "zipwith0 f [] [] = []" |
+    "zipwith0 f (x#xs) (y#ys) = f x y # zipwith0 f xs ys" |
+    "zipwith0 f (x#xs) [] = f x 0 # zipwith0 f xs []" |
+    "zipwith0 f [] (y#ys) = f 0 y # zipwith0 f [] ys"
 
 instantiation list :: ("{zero, plus}") plus
 begin
@@ -58,44 +58,44 @@
 end
 
 lemma zipwith0_Nil[simp]: "zipwith0 f [] ys = map (f 0) ys"
-by(induct ys) simp_all
+  by(induct ys) simp_all
 
 lemma list_add_Nil[simp]: "[] + xs = (xs::'a::monoid_add list)"
-by (induct xs) (auto simp:list_add_def)
+  by (induct xs) (auto simp:list_add_def)
 
 lemma list_add_Nil2[simp]: "xs + [] = (xs::'a::monoid_add list)"
-by (induct xs) (auto simp:list_add_def)
+  by (induct xs) (auto simp:list_add_def)
 
 lemma list_add_Cons[simp]: "(x#xs) + (y#ys) = (x+y)#(xs+ys)"
-by(auto simp:list_add_def)
+  by(auto simp:list_add_def)
 
 lemma list_diff_Nil[simp]: "[] - xs = -(xs::'a::group_add list)"
-by (induct xs) (auto simp:list_diff_def list_uminus_def)
+  by (induct xs) (auto simp:list_diff_def list_uminus_def)
 
 lemma list_diff_Nil2[simp]: "xs - [] = (xs::'a::group_add list)"
-by (induct xs) (auto simp:list_diff_def)
+  by (induct xs) (auto simp:list_diff_def)
 
 lemma list_diff_Cons_Cons[simp]: "(x#xs) - (y#ys) = (x-y)#(xs-ys)"
-by (induct xs) (auto simp:list_diff_def)
+  by (induct xs) (auto simp:list_diff_def)
 
 lemma list_uminus_Cons[simp]: "-(x#xs) = (-x)#(-xs)"
-by (induct xs) (auto simp:list_uminus_def)
+  by (induct xs) (auto simp:list_uminus_def)
 
 lemma self_list_diff:
   "xs - xs = replicate (length(xs::'a::group_add list)) 0"
-by(induct xs) simp_all
+  by(induct xs) simp_all
 
-lemma list_add_assoc: fixes xs :: "'a::monoid_add list"
-shows "(xs+ys)+zs = xs+(ys+zs)"
-apply(induct xs arbitrary: ys zs)
- apply simp
-apply(case_tac ys)
- apply(simp)
-apply(simp)
-apply(case_tac zs)
- apply(simp)
-apply(simp add: add.assoc)
-done
+lemma list_add_assoc: 
+  fixes xs :: "'a::monoid_add list"
+  shows "(xs+ys)+zs = xs+(ys+zs)"
+proof (induct xs arbitrary: ys zs)
+  case Nil
+  then show ?case by simp
+next
+  case (Cons a xs ys zs)
+  show ?case
+    by (cases ys; cases zs; simp add: add.assoc Cons)
+qed
 
 subsection "Inner product"
 
@@ -103,50 +103,55 @@
   where "\<langle>xs,ys\<rangle> = (\<Sum>(x,y) \<leftarrow> zip xs ys. x*y)"
 
 lemma iprod_Nil[simp]: "\<langle>[],ys\<rangle> = 0"
-by(simp add: iprod_def)
+  by(simp add: iprod_def)
 
 lemma iprod_Nil2[simp]: "\<langle>xs,[]\<rangle> = 0"
-by(simp add: iprod_def)
+  by(simp add: iprod_def)
 
 lemma iprod_Cons[simp]: "\<langle>x#xs,y#ys\<rangle> = x*y + \<langle>xs,ys\<rangle>"
-by(simp add: iprod_def)
+  by(simp add: iprod_def)
 
 lemma iprod0_if_coeffs0: "\<forall>c\<in>set cs. c = 0 \<Longrightarrow> \<langle>cs,xs\<rangle> = 0"
-apply(induct cs arbitrary:xs)
- apply simp
-apply(case_tac xs) apply simp
-apply auto
-done
+proof (induct cs arbitrary: xs)
+  case Nil
+  then show ?case by simp
+next
+  case (Cons a cs xs)
+  then show ?case
+    by (cases xs; fastforce)
+qed
 
 lemma iprod_uminus[simp]: "\<langle>-xs,ys\<rangle> = -\<langle>xs,ys\<rangle>"
-by(simp add: iprod_def uminus_sum_list_map o_def split_def map_zip_map list_uminus_def)
+  by(simp add: iprod_def uminus_sum_list_map o_def split_def map_zip_map list_uminus_def)
 
 lemma iprod_left_add_distrib: "\<langle>xs + ys,zs\<rangle> = \<langle>xs,zs\<rangle> + \<langle>ys,zs\<rangle>"
-apply(induct xs arbitrary: ys zs)
-apply (simp add: o_def split_def)
-apply(case_tac ys)
-apply simp
-apply(case_tac zs)
-apply (simp)
-apply(simp add: distrib_right)
-done
+proof (induct xs arbitrary: ys zs)
+  case Nil
+  then show ?case by simp
+next
+  case (Cons a xs ys zs)
+  show ?case
+    by (cases ys; cases zs; simp add: distrib_right Cons)
+qed
 
 lemma iprod_left_diff_distrib: "\<langle>xs - ys, zs\<rangle> = \<langle>xs,zs\<rangle> - \<langle>ys,zs\<rangle>"
-apply(induct xs arbitrary: ys zs)
-apply (simp add: o_def split_def)
-apply(case_tac ys)
-apply simp
-apply(case_tac zs)
-apply (simp)
-apply(simp add: left_diff_distrib)
-done
+proof (induct xs arbitrary: ys zs)
+  case Nil
+  then show ?case by simp
+next
+  case (Cons a xs ys zs)
+  show ?case
+    by (cases ys; cases zs; simp add: left_diff_distrib Cons)
+qed
 
 lemma iprod_assoc: "\<langle>x *\<^sub>s xs, ys\<rangle> = x * \<langle>xs,ys\<rangle>"
-apply(induct xs arbitrary: ys)
-apply simp
-apply(case_tac ys)
-apply (simp)
-apply (simp add: distrib_left mult.assoc)
-done
+proof (induct xs arbitrary: ys)
+  case Nil
+  then show ?case by simp
+next
+  case (Cons a xs ys)
+  show ?case
+    by (cases ys; simp add: distrib_left mult.assoc Cons)
+qed
 
 end
--- a/src/HOL/Library/Poly_Mapping.thy	Fri Jan 17 20:30:01 2025 +0100
+++ b/src/HOL/Library/Poly_Mapping.thy	Fri Jan 17 21:30:08 2025 +0100
@@ -20,19 +20,13 @@
   fixes f :: "'b \<Rightarrow> 'a :: mult_zero"
   assumes "finite {a. f a \<noteq> 0}"
   shows "finite {a. g a * f a \<noteq> 0}"
-proof -
-  have "{a. g a * f a \<noteq> 0} \<subseteq> {a. f a \<noteq> 0}" by auto
-  then show ?thesis using assms by (rule finite_subset)
-qed
+  by (metis (mono_tags, lifting) Collect_mono assms mult_zero_right finite_subset)
 
 lemma finite_mult_not_eq_zero_rightI:
   fixes f :: "'b \<Rightarrow> 'a :: mult_zero"
   assumes "finite {a. f a \<noteq> 0}"
   shows "finite {a. f a * g a \<noteq> 0}"
-proof -
-  have "{a. f a * g a \<noteq> 0} \<subseteq> {a. f a \<noteq> 0}" by auto
-  then show ?thesis using assms by (rule finite_subset)
-qed
+  by (metis (mono_tags, lifting) Collect_mono assms lambda_zero finite_subset)
 
 lemma finite_mult_not_eq_zero_prodI:
   fixes f g :: "'a \<Rightarrow> 'b::semiring_0"
@@ -227,10 +221,7 @@
 typedef (overloaded) ('a, 'b) poly_mapping (\<open>(_ \<Rightarrow>\<^sub>0 /_)\<close> [1, 0] 0) =
   "{f :: 'a \<Rightarrow> 'b::zero. finite {x. f x \<noteq> 0}}"
   morphisms lookup Abs_poly_mapping
-proof -
-  have "(\<lambda>_::'a. (0 :: 'b)) \<in> ?poly_mapping" by simp
-  then show ?thesis by (blast intro!: exI)
-qed
+  using not_finite_existsD by force
 
 declare lookup_inverse [simp]
 declare lookup_inject [simp]
@@ -366,9 +357,8 @@
 
 end
 
-lemma lookup_add:
-  "lookup (f + g) k = lookup f k + lookup g k"
-  by transfer rule
+lemma lookup_add: "lookup (f + g) k = lookup f k + lookup g k"
+  by (simp add: plus_poly_mapping.rep_eq)
 
 instance poly_mapping :: (type, comm_monoid_add) comm_monoid_add
   by intro_classes (transfer, simp add: fun_eq_iff ac_simps)+
@@ -435,13 +425,12 @@
 
 end
 
-lemma lookup_one:
-  "lookup 1 k = (1 when k = 0)"
-  by transfer rule
+lemma lookup_one: "lookup 1 k = (1 when k = 0)"
+  by (meson one_poly_mapping.rep_eq)
 
 lemma lookup_one_zero [simp]:
   "lookup 1 0 = 1"
-  by transfer simp
+  by (simp add: one_poly_mapping.rep_eq)
 
 definition prod_fun :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a::monoid_add \<Rightarrow> 'b::semiring_0"
 where
@@ -455,8 +444,9 @@
 proof -
   let ?C = "{a. f a \<noteq> 0} \<times> {b. g b \<noteq> 0}"
   from fin_f fin_g have "finite ?C" by blast
-  moreover have "{a. \<exists>b. (f a * g b when k = a + b) \<noteq> 0} \<times>
-    {b. \<exists>a. (f a * g b when k = a + b) \<noteq> 0} \<subseteq> {a. f a \<noteq> 0} \<times> {b. g b \<noteq> 0}"
+  moreover 
+  have "{a. \<exists>b. (f a * g b when k = a + b) \<noteq> 0} \<times>
+        {b. \<exists>a. (f a * g b when k = a + b) \<noteq> 0} \<subseteq> {a. f a \<noteq> 0} \<times> {b. g b \<noteq> 0}"
     by auto
   ultimately show ?thesis using fin_g
     by (auto simp: prod_fun_def
@@ -653,7 +643,7 @@
   show "1 * a = a"
     by transfer (simp add: prod_fun_def [abs_def] when_mult)
   show "a * 1 = a"
-    apply transfer
+    apply transfer 
     apply (simp add: prod_fun_def [abs_def] Sum_any_right_distrib Sum_any_left_distrib mult_when)
     apply (subst when_commute)
     apply simp
@@ -705,11 +695,11 @@
 
 lemma lookup_single_eq [simp]:
   "lookup (single k v) k = v"
-  by transfer simp
+  by (simp add: single.rep_eq)
 
 lemma lookup_single_not_eq:
   "k \<noteq> k' \<Longrightarrow> lookup (single k v) k' = 0"
-  by transfer simp
+  by (simp add: single.rep_eq)
 
 lemma single_zero [simp]:
   "single k 0 = 0"
@@ -749,11 +739,7 @@
 
 lemma lookup_of_nat:
   "lookup (of_nat n) k = (of_nat n when k = 0)"
-proof -
-  have "lookup (of_nat n) k = lookup (single 0 (of_nat n)) k"
-    by simp
-  then show ?thesis unfolding lookup_single by simp
-qed
+  by (metis lookup_single lookup_single_not_eq single_of_nat)
 
 lemma of_nat_single:
   "of_nat = single 0 \<circ> of_nat"
@@ -923,14 +909,7 @@
   fix f g h :: "'a \<Rightarrow> 'b"
   assume *: "less_fun f g \<or> f = g"
   have "less_fun (\<lambda>k. h k + f k) (\<lambda>k. h k + g k)" if "less_fun f g"
-  proof -
-    from that obtain k where "f k < g k" "(\<And>k'. k' < k \<Longrightarrow> f k' = g k')"
-      by (blast elim!: less_funE)
-    then have "h k + f k < h k + g k" "(\<And>k'. k' < k \<Longrightarrow> h k' + f k' = h k' + g k')"
-      by simp_all
-    then show ?thesis
-      by (blast intro: less_funI)
-  qed
+    by (metis (no_types, lifting) less_fun_def add_strict_left_mono that)
   with * show "less_fun (\<lambda>k. h k + f k) (\<lambda>k. h k + g k) \<or> (\<lambda>k. h k + f k) = (\<lambda>k. h k + g k)"
     by (auto simp: fun_eq_iff)
 qed
@@ -986,7 +965,7 @@
   have "Set.range f - {0} \<subseteq> f ` {x. f x \<noteq> 0}"
     by auto
   thus "finite (Set.range f - {0})"
-    by(rule finite_subset)(rule finite_imageI[OF *])
+    using "*" finite_surj by blast
 qed
 
 lemma in_keys_lookup_in_range [simp]:
@@ -994,7 +973,7 @@
   by transfer simp
 
 lemma in_keys_iff: "x \<in> (keys s) = (lookup s x \<noteq> 0)"
-  by (transfer, simp)
+  by (simp add: lookup_not_eq_zero_eq_in_keys)
 
 lemma keys_zero [simp]:
   "keys 0 = {}"
@@ -1221,9 +1200,9 @@
   fix g :: "'c \<Rightarrow> 'd" and p :: "'a \<Rightarrow> 'c"
   assume "finite {x. p x \<noteq> 0}"
   hence "finite (f ` {y. p (f y) \<noteq> 0})"
-    by(rule finite_subset[rotated]) auto
+    by (simp add: rev_finite_subset subset_eq)
   thus "finite {x. (p \<circ> f) x \<noteq> 0}" unfolding o_def
-    by(rule finite_imageD)(rule subset_inj_on[OF inj_f], simp)
+    by (metis finite_imageD injD inj_f inj_on_def)
 qed
 
 end
@@ -1402,7 +1381,7 @@
 
 lemma nth_trailing_zeros [simp]:
   "nth (xs @ replicate n 0) = nth xs"
-  by transfer simp
+  by (simp add: nth.abs_eq)
 
 lemma nth_idem:
   "nth (List.map (lookup f) [0..<degree f]) = f"
@@ -1454,7 +1433,7 @@
 
 lemma lookup_the_value:
   "lookup (the_value xs) k = (case map_of xs k of None \<Rightarrow> 0 | Some v \<Rightarrow> v)"
-  by transfer rule
+  by (simp add: the_value.rep_eq)
 
 lemma items_the_value:
   assumes "sorted (List.map fst xs)" and "distinct (List.map fst xs)" and "0 \<notin> snd ` set xs"
@@ -1552,15 +1531,10 @@
 proof -
   from assms obtain k where *: "lookup m k = v" "v \<noteq> 0"
     by transfer blast
-  from * have "k \<in> keys m"
+  then have "k \<in> keys m"
     by (simp add: in_keys_iff)
-  then show ?thesis
-  proof (rule poly_mapping_size_estimation)
-    from assms * have "y \<le> g (lookup m k)"
-      by simp
-    then show "y \<le> f k + g (lookup m k)"
-      by simp
-  qed
+  with * show ?thesis
+    by (simp add: Poly_Mapping.poly_mapping_size_estimation assms(2) trans_le_add2)
 qed
 
 end
@@ -1616,15 +1590,7 @@
   by (force simp add: lookup_single_not_eq)
 
 lemma frag_of_nonzero [simp]: "frag_of a \<noteq> 0"
-proof -
-  let ?f = "\<lambda>x. if x = a then 1 else (0::int)"
-  have "?f \<noteq> (\<lambda>x. 0::int)"
-    by (auto simp: fun_eq_iff)
-  then have "Poly_Mapping.lookup (Abs_poly_mapping ?f) \<noteq> Poly_Mapping.lookup (Abs_poly_mapping (\<lambda>x. 0))"
-    by fastforce
-  then show ?thesis
-    by (metis lookup_single_eq lookup_zero)
-qed
+  by (metis lookup_single_eq lookup_zero zero_neq_one)
 
 definition frag_cmul :: "int \<Rightarrow> ('a \<Rightarrow>\<^sub>0 int) \<Rightarrow> ('a \<Rightarrow>\<^sub>0 int)"
   where "frag_cmul c a = Abs_poly_mapping (\<lambda>x. c * Poly_Mapping.lookup a x)"
@@ -1636,7 +1602,7 @@
   by (simp add: frag_cmul_def)
 
 lemma frag_cmul_one [simp]: "frag_cmul 1 x = x"
-  by (auto simp: frag_cmul_def Poly_Mapping.poly_mapping.lookup_inverse)
+  by (simp add: frag_cmul_def)
 
 lemma frag_cmul_minus_one [simp]: "frag_cmul (-1) x = -x"
   by (simp add: frag_cmul_def uminus_poly_mapping_def poly_mapping_eqI)
@@ -1684,13 +1650,7 @@
   by (simp add: frag_cmul_def plus_poly_mapping_def int_distrib)
 
 lemma frag_cmul_distrib2: "frag_cmul c (a+b) = frag_cmul c a + frag_cmul c b"
-proof -
-  have "finite {x. poly_mapping.lookup a x + poly_mapping.lookup b x \<noteq> 0}"
-    using keys_add [of a b]
-    by (metis (no_types, lifting) finite_keys finite_subset keys.rep_eq lookup_add mem_Collect_eq subsetI)
-  then show ?thesis
-    by (simp add: frag_cmul_def plus_poly_mapping_def int_distrib)
-qed
+  by (simp add: int_distrib(2) lookup_add poly_mapping_eqI)
 
 lemma frag_cmul_diff_distrib: "frag_cmul (a - b) c = frag_cmul a c - frag_cmul b c"
   by (auto simp: left_diff_distrib lookup_minus poly_mapping_eqI)
--- a/src/HOL/Library/Signed_Division.thy	Fri Jan 17 20:30:01 2025 +0100
+++ b/src/HOL/Library/Signed_Division.thy	Fri Jan 17 21:30:08 2025 +0100
@@ -104,8 +104,7 @@
     "(a :: int) sdiv 1 = a"
     "(a :: int) sdiv 0 = 0"
     "(a :: int) sdiv -1 = -a"
-  apply (auto simp: signed_divide_int_def sgn_if)
-  done
+  by (auto simp: signed_divide_int_def sgn_if)
 
 lemma smod_int_mod_0 [simp]:
   "x smod (0 :: int) = x"
@@ -120,33 +119,26 @@
   by (auto simp: signed_divide_int_def sgn_div_eq_sgn_mult sgn_mult)
 
 lemma int_sdiv_same_is_1 [simp]:
-    "a \<noteq> 0 \<Longrightarrow> ((a :: int) sdiv b = a) = (b = 1)"
-  apply (rule iffI)
-   apply (clarsimp simp: signed_divide_int_def)
-   apply (subgoal_tac "b > 0")
-    apply (case_tac "a > 0")
-     apply (clarsimp simp: sgn_if)
-  apply (simp_all add: not_less algebra_split_simps sgn_if split: if_splits)
-  using int_div_less_self [of a b] apply linarith
-    apply (metis add.commute add.inverse_inverse group_cancel.rule0 int_div_less_self linorder_neqE_linordered_idom neg_0_le_iff_le not_less verit_comp_simplify1(1) zless_imp_add1_zle)
-   apply (metis div_minus_right neg_imp_zdiv_neg_iff neg_le_0_iff_le not_less order.not_eq_order_implies_strict)
-  apply (metis abs_le_zero_iff abs_of_nonneg neg_imp_zdiv_nonneg_iff order.not_eq_order_implies_strict)
-  done
+  assumes "a \<noteq> 0"
+  shows  "((a :: int) sdiv b = a) = (b = 1)"
+proof -
+  have "b = 1" if "a sdiv b = a"
+  proof -
+    have "b>0"
+      by (smt (verit, ccfv_threshold) assms mult_cancel_left2 sgn_if sgn_mult
+          sgn_sdiv_eq_sgn_mult that)
+    then show ?thesis
+      by (smt (verit) assms dvd_eq_mod_eq_0 int_div_less_self of_bool_eq(1,2) sgn_if
+          signed_divide_int_eq_divide_int that zdiv_zminus1_eq_if)
+  qed
+  then show ?thesis
+    by auto
+qed
 
 lemma int_sdiv_negated_is_minus1 [simp]:
     "a \<noteq> 0 \<Longrightarrow> ((a :: int) sdiv b = - a) = (b = -1)"
-  apply (clarsimp simp: signed_divide_int_def)
-  apply (rule iffI)
-   apply (subgoal_tac "b < 0")
-    apply (case_tac "a > 0")
-     apply (clarsimp simp: sgn_if algebra_split_simps not_less)
-     apply (case_tac "sgn (a * b) = -1")
-      apply (simp_all add: not_less algebra_split_simps sgn_if split: if_splits)
-     apply (metis add.inverse_inverse int_div_less_self int_one_le_iff_zero_less less_le neg_0_less_iff_less)
-    apply (metis add.inverse_inverse div_minus_right int_div_less_self int_one_le_iff_zero_less less_le neg_0_less_iff_less)
-   apply (metis less_le neg_less_0_iff_less not_less pos_imp_zdiv_neg_iff)
-  apply (metis div_minus_right dual_order.eq_iff neg_imp_zdiv_nonneg_iff neg_less_0_iff_less)
-  done
+  using int_sdiv_same_is_1 [of _ "-b"]
+  using signed_divide_int_def by fastforce
 
 lemma sdiv_int_range:
   \<open>a sdiv b \<in> {- \<bar>a\<bar>..\<bar>a\<bar>}\<close> for a b :: int
@@ -178,9 +170,8 @@
    "\<lbrakk> 0 \<le> a; b < 0 \<rbrakk> \<Longrightarrow> 0 \<le> (a :: int) smod b"
    "\<lbrakk> a \<le> 0; b < 0 \<rbrakk> \<Longrightarrow> (a :: int) smod b \<le> 0"
    "\<lbrakk> a \<le> 0; b < 0 \<rbrakk> \<Longrightarrow> b \<le> (a :: int) smod b"
-  apply (insert smod_int_range [where a=a and b=b])
-  apply (auto simp: add1_zle_eq smod_int_alt_def sgn_if)
-  done
+  using smod_int_range [where a=a and b=b]
+  by (auto simp: add1_zle_eq smod_int_alt_def sgn_if)
 
 lemma smod_mod_positive:
     "\<lbrakk> 0 \<le> (a :: int); 0 \<le> b \<rbrakk> \<Longrightarrow> a smod b = a mod b"
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Suc_Notation.thy	Fri Jan 17 21:30:08 2025 +0100
@@ -0,0 +1,134 @@
+(*  Title:      HOL/Library/Suc_Notation.thy
+    Author:     Manuel Eberl and Tobias Nipkow
+
+Compact notation for nested \<open>Suc\<close> terms. Just notation. Use standard numerals for large numbers.
+*)
+
+theory Suc_Notation
+imports Main
+begin
+
+text \<open>Nested \<open>Suc\<close> terms of depth \<open>2 \<le> n \<le> 9\<close> are abbreviated with new notations \<open>Suc\<^sup>n\<close>:\<close>
+
+abbreviation (input) Suc2 where "Suc2 n \<equiv> Suc (Suc n)"
+abbreviation (input) Suc3 where "Suc3 n \<equiv> Suc (Suc2 n)"
+abbreviation (input) Suc4 where "Suc4 n \<equiv> Suc (Suc3 n)"
+abbreviation (input) Suc5 where "Suc5 n \<equiv> Suc (Suc4 n)"
+abbreviation (input) Suc6 where "Suc6 n \<equiv> Suc (Suc5 n)"
+abbreviation (input) Suc7 where "Suc7 n \<equiv> Suc (Suc6 n)"
+abbreviation (input) Suc8 where "Suc8 n \<equiv> Suc (Suc7 n)"
+abbreviation (input) Suc9 where "Suc9 n \<equiv> Suc (Suc8 n)"
+
+notation Suc2 ("Suc\<^sup>2")
+notation Suc3 ("Suc\<^sup>3")
+notation Suc4 ("Suc\<^sup>4")
+notation Suc5 ("Suc\<^sup>5")
+notation Suc6 ("Suc\<^sup>6")
+notation Suc7 ("Suc\<^sup>7")
+notation Suc8 ("Suc\<^sup>8")
+notation Suc9 ("Suc\<^sup>9")
+
+text \<open>Beyond 9, the syntax \<open>Suc\<^bsup>n\<^esup>\<close> kicks in:\<close>
+
+syntax
+  "_Suc_tower" :: "num_token \<Rightarrow> nat \<Rightarrow> nat"  ("Suc\<^bsup>_\<^esup>")
+
+parse_translation \<open>
+  let
+    fun mk_sucs_aux 0 t = t
+      | mk_sucs_aux n t = mk_sucs_aux (n - 1) (\<^const>\<open>Suc\<close> $ t)
+    fun mk_sucs n = Abs("n", \<^typ>\<open>nat\<close>, mk_sucs_aux n (Bound 0))
+
+    fun Suc_tr [Free (str, _)] = mk_sucs (the (Int.fromString str))
+
+  in [(\<^syntax_const>\<open>_Suc_tower\<close>, K Suc_tr)] end
+\<close>
+
+print_translation \<open>
+  let
+    val digit_consts =
+        [\<^const_syntax>\<open>Suc2\<close>, \<^const_syntax>\<open>Suc3\<close>, \<^const_syntax>\<open>Suc4\<close>, \<^const_syntax>\<open>Suc5\<close>,
+         \<^const_syntax>\<open>Suc6\<close>, \<^const_syntax>\<open>Suc7\<close>, \<^const_syntax>\<open>Suc8\<close>, \<^const_syntax>\<open>Suc9\<close>]
+    val num_token_T = Simple_Syntax.read_typ "num_token"
+    val T = num_token_T --> HOLogic.natT --> HOLogic.natT
+    fun mk_num_token n = Free (Int.toString n, num_token_T)
+    fun dest_Suc_tower (Const (\<^const_syntax>\<open>Suc\<close>, _) $ t) acc =
+          dest_Suc_tower t (acc + 1)
+      | dest_Suc_tower t acc = (t, acc)
+
+    fun Suc_tr' [t] =
+      let
+        val (t', n) = dest_Suc_tower t 1
+      in
+        if n > 9 then
+          Const (\<^syntax_const>\<open>_Suc_tower\<close>, T) $ mk_num_token n $ t'
+        else if n > 1 then
+          Const (List.nth (digit_consts, n - 2), T) $ t'
+        else
+          raise Match
+      end
+
+  in [(\<^const_syntax>\<open>Suc\<close>, K Suc_tr')]
+ end
+\<close>
+
+(* Tests
+
+ML \<open>
+local
+  fun mk 0 = \<^term>\<open>x :: nat\<close>
+    | mk n = \<^const>\<open>Suc\<close> $ mk (n - 1)
+  val ctxt' = Variable.add_fixes_implicit @{term "x :: nat"} @{context}
+in
+  val _ =
+    map_range (fn n => (n + 1, mk (n + 1))) 20
+    |> map (fn (n, t) => 
+         Pretty.block [Pretty.str (Int.toString n ^ ": "),
+           Syntax.pretty_term ctxt' t] |> Pretty.writeln)
+end
+\<close>
+
+(* test parsing *)
+term "Suc x"
+term "Suc\<^sup>2 x"
+term "Suc\<^sup>3 x"
+term "Suc\<^sup>4 x"
+term "Suc\<^sup>5 x"
+term "Suc\<^sup>6 x"
+term "Suc\<^sup>7 x"
+term "Suc\<^sup>8 x"
+term "Suc\<^sup>9 x"
+
+term "Suc\<^bsup>2\<^esup> x"
+term "Suc\<^bsup>3\<^esup> x"
+term "Suc\<^bsup>4\<^esup> x"
+term "Suc\<^bsup>5\<^esup> x"
+term "Suc\<^bsup>6\<^esup> x"
+term "Suc\<^bsup>7\<^esup> x"
+term "Suc\<^bsup>8\<^esup> x"
+term "Suc\<^bsup>9\<^esup> x"
+term "Suc\<^bsup>10\<^esup> x"
+term "Suc\<^bsup>11\<^esup> x"
+term "Suc\<^bsup>12\<^esup> x"
+term "Suc\<^bsup>13\<^esup> x"
+term "Suc\<^bsup>14\<^esup> x"
+term "Suc\<^bsup>15\<^esup> x"
+term "Suc\<^bsup>16\<^esup> x"
+term "Suc\<^bsup>17\<^esup> x"
+term "Suc\<^bsup>18\<^esup> x"
+term "Suc\<^bsup>19\<^esup> x"
+term "Suc\<^bsup>20\<^esup> x"
+
+(* check that the notation really means the right thing *)
+lemma "Suc\<^sup>2 n = n+2 \<and> Suc\<^sup>3 n = n+3 \<and> Suc\<^sup>4 n = n+4 \<and> Suc\<^sup>5 n = n+5
+  \<and> Suc\<^sup>6 n = n+6 \<and> Suc\<^sup>7 n = n+7 \<and> Suc\<^sup>8 n = n+8 \<and> Suc\<^sup>9 n = n+9"
+by simp
+
+lemma "Suc\<^bsup>10\<^esup> n = n+10 \<and> Suc\<^bsup>11\<^esup> n = n+11 \<and> Suc\<^bsup>12\<^esup> n = n+12 \<and> Suc\<^bsup>13\<^esup> n = n+13
+  \<and> Suc\<^bsup>14\<^esup> n = n+14 \<and> Suc\<^bsup>15\<^esup> n = n+15 \<and> Suc\<^bsup>16\<^esup> n = n+16 \<and> Suc\<^bsup>17\<^esup> n = n+17
+  \<and> Suc\<^bsup>18\<^esup> n = n+18 \<and> Suc\<^bsup>19\<^esup> n = n+19 \<and> Suc\<^bsup>20\<^esup> n = n+20"
+by simp
+
+*)
+
+end
\ No newline at end of file
--- a/src/HOL/ROOT	Fri Jan 17 20:30:01 2025 +0100
+++ b/src/HOL/ROOT	Fri Jan 17 21:30:08 2025 +0100
@@ -88,6 +88,7 @@
     RBT_Set
     (*printing modifications*)
     OptionalSugar
+    Suc_Notation
     (*prototypic tools*)
     Predicate_Compile_Quickcheck
     (*legacy tools*)
--- a/src/HOL/Tools/BNF/bnf_def.ML	Fri Jan 17 20:30:01 2025 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Fri Jan 17 21:30:08 2025 +0100
@@ -59,6 +59,7 @@
   val bd_card_order_of_bnf: bnf -> thm
   val bd_cinfinite_of_bnf: bnf -> thm
   val bd_regularCard_of_bnf: bnf -> thm
+  val bd_def_of_bnf: bnf -> thm
   val collect_set_map_of_bnf: bnf -> thm
   val in_bd_of_bnf: bnf -> thm
   val in_cong_of_bnf: bnf -> thm
@@ -251,14 +252,15 @@
 type defs = {
   map_def: thm,
   set_defs: thm list,
+  bd_def: thm,
   rel_def: thm,
   pred_def: thm
 }
 
-fun mk_defs map sets rel pred = {map_def = map, set_defs = sets, rel_def = rel, pred_def = pred};
+fun mk_defs map sets bd rel pred = {map_def = map, bd_def = bd, set_defs = sets, rel_def = rel, pred_def = pred};
 
-fun map_defs f {map_def, set_defs, rel_def, pred_def} =
-  {map_def = f map_def, set_defs = map f set_defs, rel_def = f rel_def, pred_def = f pred_def};
+fun map_defs f {map_def, set_defs, bd_def, rel_def, pred_def} =
+  {map_def = f map_def, set_defs = map f set_defs, bd_def = f bd_def, rel_def = f rel_def, pred_def = f pred_def};
 
 val morph_defs = map_defs o Morphism.thm;
 
@@ -582,6 +584,7 @@
 val bd_card_order_of_bnf = #bd_card_order o #axioms o rep_bnf;
 val bd_cinfinite_of_bnf = #bd_cinfinite o #axioms o rep_bnf;
 val bd_regularCard_of_bnf = #bd_regularCard o #axioms o rep_bnf;
+val bd_def_of_bnf = #bd_def o #defs o rep_bnf;
 val collect_set_map_of_bnf = Lazy.force o #collect_set_map o #facts o rep_bnf;
 val in_bd_of_bnf = Lazy.force o #in_bd o #facts o rep_bnf;
 val in_cong_of_bnf = Lazy.force o #in_cong o #facts o rep_bnf;
@@ -1005,8 +1008,10 @@
     val notes =
       [(mk_def_binding map_of_bnf, map_def_of_bnf bnf),
        (mk_def_binding rel_of_bnf, rel_def_of_bnf bnf),
+       (mk_def_binding bd_of_bnf, bd_def_of_bnf bnf),
        (mk_def_binding pred_of_bnf, pred_def_of_bnf bnf)] @
       @{map 2} (pair o mk_def_binding o K) (sets_of_bnf bnf) (set_defs_of_bnf bnf)
+      |> filter_out (fn (b, thm) => Thm.is_reflexive thm)
       |> map (fn (b, thm) => ((b, []), [([thm], [])]));
   in
     lthy
@@ -2042,7 +2047,7 @@
 
         val inj_map_strong = Lazy.lazy mk_inj_map_strong;
 
-        val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def bnf_pred_def;
+        val defs = mk_defs bnf_map_def bnf_set_defs bnf_bd_def bnf_rel_def bnf_pred_def;
 
         val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong
           in_mono in_rel inj_map inj_map_strong map_comp map_cong map_cong_simp map_cong_pred map_id
--- a/src/HOL/Tools/BNF/bnf_lift.ML	Fri Jan 17 20:30:01 2025 +0100
+++ b/src/HOL/Tools/BNF/bnf_lift.ML	Fri Jan 17 21:30:08 2025 +0100
@@ -436,7 +436,7 @@
 
     (* get the bnf for RepT *)
     val ((bnf_F, (deads, alphas)), ((_, unfolds), lthy)) =
-      bnf_of_typ true Dont_Inline (Binding.qualify true AbsT_name) flatten_tyargs []
+      bnf_of_typ true Hardly_Inline (Binding.qualify true AbsT_name) flatten_tyargs []
         Ds0 RepT ((empty_comp_cache, empty_unfolds), lthy);
 
     val set_bs =
@@ -670,7 +670,7 @@
               [card_order_bd_tac, cinfinite_bd_tac, regularCard_bd_tac] @ set_bds_tac @
               [le_rel_OO_tac, rel_OO_Grp_tac, pred_set_tac];
 
-            val (bnf_G, lthy) = bnf_def Dont_Inline (user_policy Note_Some) true I
+            val (bnf_G, lthy) = bnf_def Hardly_Inline (user_policy Note_Some) true I
               tactics wit_tac NONE map_b rel_b pred_b set_bs
               (((((((Binding.empty, AbsT), map_G), sets_G), bd_G), wits_G), SOME rel_G), SOME pred_G)
               lthy;
@@ -852,7 +852,7 @@
       map dest_TFree alpha0s |> filter (fn T => exists (fn Ts => member op= Ts T) Ass);
 
     val ((bnf_F, (deads, alphas)), ((_, unfolds), lthy)) =
-      bnf_of_typ true Dont_Inline (Binding.qualify true absT_name) flatten_tyargs
+      bnf_of_typ true Hardly_Inline (Binding.qualify true absT_name) flatten_tyargs
         [] Ds0 repT ((empty_comp_cache, empty_unfolds), lthy);
     val live = length alphas;
     val _ = (if live = 0 then error "No live variables" else ());
@@ -1889,7 +1889,7 @@
             | mk_wit_tacs [] ws ctxt = mk_wit_tacs set_F'_thmss ws ctxt
             | mk_wit_tacs _ _ _ = all_tac;
 
-          val (bnf_G, lthy) = bnf_def Dont_Inline (user_policy Note_Some) true I
+          val (bnf_G, lthy) = bnf_def Hardly_Inline (user_policy Note_Some) true I
             tactics (mk_wit_tacs [] wit_thms) NONE map_b rel_b pred_b set_bs
             (((((((Binding.empty, absT), map_G), sets_G), bd_G), wits_G), SOME rel_G), NONE) lthy;
 
--- a/src/HOL/Tools/inductive.ML	Fri Jan 17 20:30:01 2025 +0100
+++ b/src/HOL/Tools/inductive.ML	Fri Jan 17 21:30:08 2025 +0100
@@ -21,7 +21,7 @@
 signature INDUCTIVE =
 sig
   type result =
-    {preds: term list, elims: thm list, raw_induct: thm,
+    {preds: term list, elims: thm list, raw_induct: thm, def: thm, mono: thm,
      induct: thm, inducts: thm list, intrs: thm list, eqs: thm list}
   val transform_result: morphism -> result -> result
   type info = {names: string list, coind: bool} * result
@@ -180,17 +180,18 @@
 (** context data **)
 
 type result =
-  {preds: term list, elims: thm list, raw_induct: thm,
+  {preds: term list, elims: thm list, raw_induct: thm, def: thm, mono: thm,
    induct: thm, inducts: thm list, intrs: thm list, eqs: thm list};
 
-fun transform_result phi {preds, elims, raw_induct: thm, induct, inducts, intrs, eqs} =
+fun transform_result phi {preds, elims, raw_induct: thm, induct, inducts, intrs, eqs, def, mono} =
   let
     val term = Morphism.term phi;
     val thm = Morphism.thm phi;
     val fact = Morphism.fact phi;
   in
-   {preds = map term preds, elims = fact elims, raw_induct = thm raw_induct,
-    induct = thm induct, inducts = fact inducts, intrs = fact intrs, eqs = fact eqs}
+   {preds = map term preds, elims = fact elims, raw_induct = thm raw_induct, def = thm def,
+    induct = thm induct, inducts = fact inducts, intrs = fact intrs, eqs = fact eqs,
+    mono = thm mono}
   end;
 
 type info = {names: string list, coind: bool} * result;
@@ -1152,6 +1153,8 @@
        raw_induct = rulify lthy3 raw_induct,
        induct = induct,
        inducts = inducts,
+       def = fp_def,
+       mono = mono,
        eqs = eqs'};
 
     val lthy4 = lthy3
--- a/src/HOL/Tools/inductive_set.ML	Fri Jan 17 20:30:01 2025 +0100
+++ b/src/HOL/Tools/inductive_set.ML	Fri Jan 17 21:30:08 2025 +0100
@@ -463,7 +463,7 @@
         eta_contract (member op = cs' orf is_pred pred_arities))) intros;
     val cnames_syn' = map (fn (b, _) => (Binding.suffix_name "p" b, NoSyn)) cnames_syn;
     val monos' = map (to_pred [] (Context.Proof lthy)) monos;
-    val ({preds, intrs, elims, raw_induct, eqs, ...}, lthy1) =
+    val ({preds, intrs, elims, raw_induct, eqs, def, mono, ...}, lthy1) =
       Inductive.add_ind_def
         {quiet_mode = quiet_mode, verbose = verbose, alt_name = Binding.empty,
           coind = coind, no_elim = no_elim, no_ind = no_ind, skip_mono = skip_mono}
@@ -513,7 +513,7 @@
         (map (to_set [] (Context.Proof lthy3)) eqs) raw_induct' lthy3;
   in
     ({intrs = intrs', elims = elims', induct = induct, inducts = inducts,
-      raw_induct = raw_induct', preds = map fst defs, eqs = eqs'},
+      raw_induct = raw_induct', preds = map fst defs, eqs = eqs', def = def, mono = mono},
      lthy4)
   end;
 
--- a/src/Pure/Build/build_schedule.scala	Fri Jan 17 20:30:01 2025 +0100
+++ b/src/Pure/Build/build_schedule.scala	Fri Jan 17 21:30:08 2025 +0100
@@ -69,14 +69,16 @@
     }
 
     def load(
+      build_options: Options,
       host_infos: Host_Infos,
       log_database: SQL.Database,
       sessions_structure: Sessions.Structure
     ): Timing_Data = {
+      val days = build_options.int("build_schedule_history")
       val build_history =
         for {
           log_name <- log_database.execute_query_statement(
-            Build_Log.private_data.meta_info_table.select(List(Build_Log.Column.log_name)),
+            Build_Log.private_data.select_recent_log_names(days),
             List.from[String], res => res.string(Build_Log.Column.log_name))
           meta_info <- Build_Log.private_data.read_meta_info(log_database, log_name)
           build_info = Build_Log.private_data.read_build_info(log_database, log_name)
@@ -1065,9 +1067,8 @@
       Host_Infos.load(build_options, build_hosts, _host_database)
     }
 
-    private val timing_data: Timing_Data = {
-      Timing_Data.load(_host_infos, _log_database, build_context.sessions_structure)
-    }
+    private val timing_data: Timing_Data =
+      Timing_Data.load(build_options, _host_infos, _log_database, build_context.sessions_structure)
 
     private var _scheduler = init_scheduler(timing_data)
 
@@ -1108,6 +1109,7 @@
       val props =
         List(
           Build_Log.Prop.build_id.name -> build_context.build_uuid,
+          Build_Log.Prop.isabelle_version.name -> Isabelle_System.isabelle_id(),
           Build_Log.Prop.build_engine.name -> build_context.engine.name,
           Build_Log.Prop.build_host.name -> hostname,
           Build_Log.Prop.build_start.name -> Build_Log.print_date(build_start))
@@ -1261,7 +1263,7 @@
 
     def read_serial(db: SQL.Database, build_uuid: String = ""): Long =
       db.execute_query_statementO[Long](
-        Schedules.table.select(List(Schedules.serial.max), sql = 
+        Schedules.table.select(List(Schedules.serial.max), sql =
           SQL.where(if_proper(build_uuid, Schedules.build_uuid.equal(build_uuid)))),
           _.long(Schedules.serial)).getOrElse(0L)
 
@@ -1373,7 +1375,7 @@
         schedule.generator != old_schedule.generator ||
         schedule.start != old_schedule.start ||
         schedule.graph != old_schedule.graph
-      
+
       val schedule1 =
         if (changed) schedule.copy(serial = old_schedule.next_serial) else schedule
       if (schedule1.serial != schedule.serial) write_schedule(db, schedule1)
@@ -1525,7 +1527,7 @@
       }
 
       val host_infos = Host_Infos.load(build_options, cluster_hosts, host_database)
-      val timing_data = Timing_Data.load(host_infos, log_database, full_sessions)
+      val timing_data = Timing_Data.load(build_options, host_infos, log_database, full_sessions)
 
       val sessions = Build_Process.Sessions.empty.init(build_context, database_server, progress)
 
--- a/src/Pure/General/mercurial.scala	Fri Jan 17 20:30:01 2025 +0100
+++ b/src/Pure/General/mercurial.scala	Fri Jan 17 21:30:08 2025 +0100
@@ -117,6 +117,9 @@
 
   /* hg_sync meta data */
 
+  def sync_id(root: Path, ssh: SSH.System = SSH.Local): Option[String] =
+    if (Hg_Sync.ok(root, ssh)) Some(Hg_Sync.directory(root, ssh).id) else None
+
   object Hg_Sync {
     val NAME = ".hg_sync"
     val _NAME: String = " " + NAME
--- a/src/Pure/System/isabelle_system.scala	Fri Jan 17 20:30:01 2025 +0100
+++ b/src/Pure/System/isabelle_system.scala	Fri Jan 17 21:30:08 2025 +0100
@@ -100,7 +100,8 @@
   def isabelle_id(root: Path = Path.ISABELLE_HOME): String =
     getetc("ISABELLE_ID", root = root) orElse
     Mercurial.archive_id(root) orElse
-    Mercurial.id_repository(root, rev = "") getOrElse
+    Mercurial.id_repository(root, rev = "") orElse
+    Mercurial.sync_id(root) getOrElse
     error("Failed to identify Isabelle distribution " + root.expand)
 
   object Isabelle_Id extends Scala.Fun_String("isabelle_id") {