# HG changeset patch # User wenzelm # Date 1737145808 -3600 # Node ID f0ae2acbefd56321aee942b99dc8dd9022ea576d # Parent e7be7c4b871c000f4734c4152c3b75b809485c93# Parent fa0bafdc0fc655b365b7f353e99979224c3421cf merged diff -r fa0bafdc0fc6 -r f0ae2acbefd5 NEWS --- 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 diff -r fa0bafdc0fc6 -r f0ae2acbefd5 etc/options --- 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" diff -r fa0bafdc0fc6 -r f0ae2acbefd5 src/HOL/Cardinals/Wellorder_Constructions.thy --- 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 \ Field r" and A: "AboveS B \ {}" and b: "b \ B" shows "b \ underS (suc B)" using suc_AboveS[OF B A] b unfolding underS_def AboveS_def by auto diff -r fa0bafdc0fc6 -r f0ae2acbefd5 src/HOL/Codegenerator_Test/Code_Test_GHC.thy --- 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 \Test cases for bit operations on target language numerals\ - -unbundle bit_operations_syntax - -lemma \bit (473514 :: integer) 5\ - by normalization - -test_code \bit (473514 :: integer) 5\ in GHC - -lemma \bit (- 805167 :: integer) 7\ - by normalization - -test_code \bit (- 805167 :: integer) 7\ in GHC - -lemma \473514 AND (767063 :: integer) = 208898\ - by normalization - -test_code \473514 AND (767063 :: integer) = 208898\ in GHC - -lemma \- 805167 AND (767063 :: integer) = 242769\ - by normalization - -test_code \- 805167 AND (767063 :: integer) = 242769\ in GHC - -lemma \473514 AND (- 314527 :: integer) = 209184\ - by normalization - -test_code \473514 AND (- 314527 :: integer) = 209184\ in GHC - -lemma \- 805167 AND (- 314527 :: integer) = - 839103\ - by normalization - -test_code \- 805167 AND (- 314527 :: integer) = - 839103\ in GHC - -lemma \473514 OR (767063 :: integer) = 1031679\ - by normalization - -test_code \473514 OR (767063 :: integer) = 1031679\ in GHC - -lemma \- 805167 OR (767063 :: integer) = - 280873\ - by normalization - -test_code \- 805167 OR (767063 :: integer) = - 280873\ in GHC - -lemma \473514 OR (- 314527 :: integer) = - 50197\ - by normalization - -test_code \473514 OR (- 314527 :: integer) = - 50197\ in GHC - -lemma \- 805167 OR (- 314527 :: integer) = - 280591\ - by normalization - -test_code \- 805167 OR (- 314527 :: integer) = - 280591\ in GHC - -lemma \473514 XOR (767063 :: integer) = 822781\ - by normalization - -test_code \473514 XOR (767063 :: integer) = 822781\ in GHC - -lemma \- 805167 XOR (767063 :: integer) = - 523642\ - by normalization - -test_code \- 805167 XOR (767063 :: integer) = - 523642\ in GHC - -lemma \473514 XOR (- 314527 :: integer) = - 259381\ - by normalization - -test_code \473514 XOR (- 314527 :: integer) = - 259381\ in GHC - -lemma \- 805167 XOR (- 314527 :: integer) = 558512\ - by normalization - -test_code \- 805167 XOR (- 314527 :: integer) = 558512\ in GHC - -lemma \NOT (473513 :: integer) = - 473514\ - by normalization - -test_code \NOT (473513 :: integer) = - 473514\ in GHC - -lemma \NOT (- 805167 :: integer) = 805166\ - by normalization - -test_code \NOT (- 805167 :: integer) = 805166\ in GHC - -lemma \(mask 39 :: integer) = 549755813887\ - by normalization - -test_code \(mask 39 :: integer) = 549755813887\ in GHC - -lemma \set_bit 15 (473514 :: integer) = 506282\ - by normalization - -test_code \set_bit 15 (473514 :: integer) = 506282\ in GHC - -lemma \set_bit 11 (- 805167 :: integer) = - 803119\ - by normalization - -test_code \set_bit 11 (- 805167 :: integer) = - 803119\ in GHC - -lemma \unset_bit 13 (473514 :: integer) = 465322\ - by normalization - -test_code \unset_bit 13 (473514 :: integer) = 465322\ in GHC - -lemma \unset_bit 12 (- 805167 :: integer) = - 809263\ - by normalization - -test_code \unset_bit 12 (- 805167 :: integer) = - 809263\ in GHC - -lemma \flip_bit 15 (473514 :: integer) = 506282\ - by normalization - -test_code \flip_bit 15 (473514 :: integer) = 506282\ in GHC - -lemma \flip_bit 12 (- 805167 :: integer) = - 809263\ - by normalization - -test_code \flip_bit 12 (- 805167 :: integer) = - 809263\ in GHC - -lemma \push_bit 12 (473514 :: integer) = 1939513344\ - by normalization - -test_code \push_bit 12 (473514 :: integer) = 1939513344\ in GHC - -lemma \push_bit 12 (- 805167 :: integer) = - 3297964032\ - by normalization - -test_code \push_bit 12 (- 805167 :: integer) = - 3297964032\ in GHC - -lemma \drop_bit 12 (473514 :: integer) = 115\ - by normalization - -test_code \drop_bit 12 (473514 :: integer) = 115\ in GHC - -lemma \drop_bit 12 (- 805167 :: integer) = - 197\ - by normalization - -test_code \drop_bit 12 (- 805167 :: integer) = - 197\ in GHC - -lemma \take_bit 12 (473514 :: integer) = 2474\ - by normalization - -test_code \take_bit 12 (473514 :: integer) = 2474\ in GHC - -lemma \take_bit 12 (- 805167 :: integer) = 1745\ - by normalization - -test_code \take_bit 12 (- 805167 :: integer) = 1745\ in GHC - -lemma \signed_take_bit 12 (473514 :: integer) = - 1622\ - by normalization - -test_code \signed_take_bit 12 (473514 :: integer) = - 1622\ in GHC - -lemma \signed_take_bit 12 (- 805167 :: integer) = - 2351\ - by normalization - -test_code \signed_take_bit 12 (- 805167 :: integer) = - 2351\ in GHC - end diff -r fa0bafdc0fc6 -r f0ae2acbefd5 src/HOL/Codegenerator_Test/Code_Test_OCaml.thy --- 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 \Test cases for bit operations on target language numerals\ - -unbundle bit_operations_syntax - -lemma \bit (473514 :: integer) 5\ - by normalization - -test_code \bit (473514 :: integer) 5\ in OCaml - -lemma \bit (- 805167 :: integer) 7\ - by normalization - -test_code \bit (- 805167 :: integer) 7\ in OCaml - -lemma \473514 AND (767063 :: integer) = 208898\ - by normalization - -test_code \473514 AND (767063 :: integer) = 208898\ in OCaml - -lemma \- 805167 AND (767063 :: integer) = 242769\ - by normalization - -test_code \- 805167 AND (767063 :: integer) = 242769\ in OCaml - -lemma \473514 AND (- 314527 :: integer) = 209184\ - by normalization - -test_code \473514 AND (- 314527 :: integer) = 209184\ in OCaml - -lemma \- 805167 AND (- 314527 :: integer) = - 839103\ - by normalization - -test_code \- 805167 AND (- 314527 :: integer) = - 839103\ in OCaml - -lemma \473514 OR (767063 :: integer) = 1031679\ - by normalization - -test_code \473514 OR (767063 :: integer) = 1031679\ in OCaml - -lemma \- 805167 OR (767063 :: integer) = - 280873\ - by normalization - -test_code \- 805167 OR (767063 :: integer) = - 280873\ in OCaml - -lemma \473514 OR (- 314527 :: integer) = - 50197\ - by normalization - -test_code \473514 OR (- 314527 :: integer) = - 50197\ in OCaml - -lemma \- 805167 OR (- 314527 :: integer) = - 280591\ - by normalization - -test_code \- 805167 OR (- 314527 :: integer) = - 280591\ in OCaml - -lemma \473514 XOR (767063 :: integer) = 822781\ - by normalization - -test_code \473514 XOR (767063 :: integer) = 822781\ in OCaml - -lemma \- 805167 XOR (767063 :: integer) = - 523642\ - by normalization - -test_code \- 805167 XOR (767063 :: integer) = - 523642\ in OCaml - -lemma \473514 XOR (- 314527 :: integer) = - 259381\ - by normalization - -test_code \473514 XOR (- 314527 :: integer) = - 259381\ in OCaml - -lemma \- 805167 XOR (- 314527 :: integer) = 558512\ - by normalization - -test_code \- 805167 XOR (- 314527 :: integer) = 558512\ in OCaml - -lemma \NOT (473513 :: integer) = - 473514\ - by normalization - -test_code \NOT (473513 :: integer) = - 473514\ in OCaml - -lemma \NOT (- 805167 :: integer) = 805166\ - by normalization - -test_code \NOT (- 805167 :: integer) = 805166\ in OCaml - -lemma \(mask 39 :: integer) = 549755813887\ - by normalization - -test_code \(mask 39 :: integer) = 549755813887\ in OCaml - -lemma \set_bit 15 (473514 :: integer) = 506282\ - by normalization - -test_code \set_bit 15 (473514 :: integer) = 506282\ in OCaml - -lemma \set_bit 11 (- 805167 :: integer) = - 803119\ - by normalization - -test_code \set_bit 11 (- 805167 :: integer) = - 803119\ in OCaml - -lemma \unset_bit 13 (473514 :: integer) = 465322\ - by normalization - -test_code \unset_bit 13 (473514 :: integer) = 465322\ in OCaml - -lemma \unset_bit 12 (- 805167 :: integer) = - 809263\ - by normalization - -test_code \unset_bit 12 (- 805167 :: integer) = - 809263\ in OCaml - -lemma \flip_bit 15 (473514 :: integer) = 506282\ - by normalization - -test_code \flip_bit 15 (473514 :: integer) = 506282\ in OCaml - -lemma \flip_bit 12 (- 805167 :: integer) = - 809263\ - by normalization - -test_code \flip_bit 12 (- 805167 :: integer) = - 809263\ in OCaml - -lemma \push_bit 12 (473514 :: integer) = 1939513344\ - by normalization - -test_code \push_bit 12 (473514 :: integer) = 1939513344\ in OCaml - -lemma \push_bit 12 (- 805167 :: integer) = - 3297964032\ - by normalization - -test_code \push_bit 12 (- 805167 :: integer) = - 3297964032\ in OCaml - -lemma \drop_bit 12 (473514 :: integer) = 115\ - by normalization - -test_code \drop_bit 12 (473514 :: integer) = 115\ in OCaml - -lemma \drop_bit 12 (- 805167 :: integer) = - 197\ - by normalization - -test_code \drop_bit 12 (- 805167 :: integer) = - 197\ in OCaml - -lemma \take_bit 12 (473514 :: integer) = 2474\ - by normalization - -test_code \take_bit 12 (473514 :: integer) = 2474\ in OCaml - -lemma \take_bit 12 (- 805167 :: integer) = 1745\ - by normalization - -test_code \take_bit 12 (- 805167 :: integer) = 1745\ in OCaml - -lemma \signed_take_bit 12 (473514 :: integer) = - 1622\ - by normalization - -test_code \signed_take_bit 12 (473514 :: integer) = - 1622\ in OCaml - -lemma \signed_take_bit 12 (- 805167 :: integer) = - 2351\ - by normalization - -test_code \signed_take_bit 12 (- 805167 :: integer) = - 2351\ in OCaml - end diff -r fa0bafdc0fc6 -r f0ae2acbefd5 src/HOL/Codegenerator_Test/Code_Test_PolyML.thy --- 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 \Test cases for bit operations on target language numerals\ - -unbundle bit_operations_syntax - -lemma \bit (473514 :: integer) 5\ - by normalization - -test_code \bit (473514 :: integer) 5\ in PolyML - -lemma \bit (- 805167 :: integer) 7\ - by normalization - -test_code \bit (- 805167 :: integer) 7\ in PolyML - -lemma \473514 AND (767063 :: integer) = 208898\ - by normalization - -test_code \473514 AND (767063 :: integer) = 208898\ in PolyML - -lemma \- 805167 AND (767063 :: integer) = 242769\ - by normalization - -test_code \- 805167 AND (767063 :: integer) = 242769\ in PolyML - -lemma \473514 AND (- 314527 :: integer) = 209184\ - by normalization - -test_code \473514 AND (- 314527 :: integer) = 209184\ in PolyML - -lemma \- 805167 AND (- 314527 :: integer) = - 839103\ - by normalization - -test_code \- 805167 AND (- 314527 :: integer) = - 839103\ in PolyML - -lemma \473514 OR (767063 :: integer) = 1031679\ - by normalization - -test_code \473514 OR (767063 :: integer) = 1031679\ in PolyML - -lemma \- 805167 OR (767063 :: integer) = - 280873\ - by normalization - -test_code \- 805167 OR (767063 :: integer) = - 280873\ in PolyML - -lemma \473514 OR (- 314527 :: integer) = - 50197\ - by normalization - -test_code \473514 OR (- 314527 :: integer) = - 50197\ in PolyML - -lemma \- 805167 OR (- 314527 :: integer) = - 280591\ - by normalization - -test_code \- 805167 OR (- 314527 :: integer) = - 280591\ in PolyML - -lemma \473514 XOR (767063 :: integer) = 822781\ - by normalization - -test_code \473514 XOR (767063 :: integer) = 822781\ in PolyML - -lemma \- 805167 XOR (767063 :: integer) = - 523642\ - by normalization - -test_code \- 805167 XOR (767063 :: integer) = - 523642\ in PolyML - -lemma \473514 XOR (- 314527 :: integer) = - 259381\ - by normalization - -test_code \473514 XOR (- 314527 :: integer) = - 259381\ in PolyML - -lemma \- 805167 XOR (- 314527 :: integer) = 558512\ - by normalization - -test_code \- 805167 XOR (- 314527 :: integer) = 558512\ in PolyML - -lemma \NOT (473513 :: integer) = - 473514\ - by normalization - -test_code \NOT (473513 :: integer) = - 473514\ in PolyML - -lemma \NOT (- 805167 :: integer) = 805166\ - by normalization - -test_code \NOT (- 805167 :: integer) = 805166\ in PolyML - -lemma \(mask 39 :: integer) = 549755813887\ - by normalization - -test_code \(mask 39 :: integer) = 549755813887\ in PolyML - -lemma \set_bit 15 (473514 :: integer) = 506282\ - by normalization - -test_code \set_bit 15 (473514 :: integer) = 506282\ in PolyML - -lemma \set_bit 11 (- 805167 :: integer) = - 803119\ - by normalization - -test_code \set_bit 11 (- 805167 :: integer) = - 803119\ in PolyML - -lemma \unset_bit 13 (473514 :: integer) = 465322\ - by normalization - -test_code \unset_bit 13 (473514 :: integer) = 465322\ in PolyML - -lemma \unset_bit 12 (- 805167 :: integer) = - 809263\ - by normalization - -test_code \unset_bit 12 (- 805167 :: integer) = - 809263\ in PolyML - -lemma \flip_bit 15 (473514 :: integer) = 506282\ - by normalization - -test_code \flip_bit 15 (473514 :: integer) = 506282\ in PolyML - -lemma \flip_bit 12 (- 805167 :: integer) = - 809263\ - by normalization - -test_code \flip_bit 12 (- 805167 :: integer) = - 809263\ in PolyML - -lemma \push_bit 12 (473514 :: integer) = 1939513344\ - by normalization - -test_code \push_bit 12 (473514 :: integer) = 1939513344\ in PolyML - -lemma \push_bit 12 (- 805167 :: integer) = - 3297964032\ - by normalization - -test_code \push_bit 12 (- 805167 :: integer) = - 3297964032\ in PolyML - -lemma \drop_bit 12 (473514 :: integer) = 115\ - by normalization - -test_code \drop_bit 12 (473514 :: integer) = 115\ in PolyML - -lemma \drop_bit 12 (- 805167 :: integer) = - 197\ - by normalization - -test_code \drop_bit 12 (- 805167 :: integer) = - 197\ in PolyML - -lemma \take_bit 12 (473514 :: integer) = 2474\ - by normalization - -test_code \take_bit 12 (473514 :: integer) = 2474\ in PolyML - -lemma \take_bit 12 (- 805167 :: integer) = 1745\ - by normalization - -test_code \take_bit 12 (- 805167 :: integer) = 1745\ in PolyML - -lemma \signed_take_bit 12 (473514 :: integer) = - 1622\ - by normalization - -test_code \signed_take_bit 12 (473514 :: integer) = - 1622\ in PolyML - -lemma \signed_take_bit 12 (- 805167 :: integer) = - 2351\ - by normalization - -test_code \signed_take_bit 12 (- 805167 :: integer) = - 2351\ in PolyML - end diff -r fa0bafdc0fc6 -r f0ae2acbefd5 src/HOL/Codegenerator_Test/Code_Test_Scala.thy --- 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 \Test cases for bit operations on target language numerals\ - -unbundle bit_operations_syntax - -lemma \bit (473514 :: integer) 5\ - by normalization - -test_code \bit (473514 :: integer) 5\ in Scala - -lemma \bit (- 805167 :: integer) 7\ - by normalization - -test_code \bit (- 805167 :: integer) 7\ in Scala - -lemma \473514 AND (767063 :: integer) = 208898\ - by normalization - -test_code \473514 AND (767063 :: integer) = 208898\ in Scala - -lemma \- 805167 AND (767063 :: integer) = 242769\ - by normalization - -test_code \- 805167 AND (767063 :: integer) = 242769\ in Scala - -lemma \473514 AND (- 314527 :: integer) = 209184\ - by normalization - -test_code \473514 AND (- 314527 :: integer) = 209184\ in Scala - -lemma \- 805167 AND (- 314527 :: integer) = - 839103\ - by normalization - -test_code \- 805167 AND (- 314527 :: integer) = - 839103\ in Scala - -lemma \473514 OR (767063 :: integer) = 1031679\ - by normalization - -test_code \473514 OR (767063 :: integer) = 1031679\ in Scala - -lemma \- 805167 OR (767063 :: integer) = - 280873\ - by normalization - -test_code \- 805167 OR (767063 :: integer) = - 280873\ in Scala - -lemma \473514 OR (- 314527 :: integer) = - 50197\ - by normalization - -test_code \473514 OR (- 314527 :: integer) = - 50197\ in Scala - -lemma \- 805167 OR (- 314527 :: integer) = - 280591\ - by normalization - -test_code \- 805167 OR (- 314527 :: integer) = - 280591\ in Scala - -lemma \473514 XOR (767063 :: integer) = 822781\ - by normalization - -test_code \473514 XOR (767063 :: integer) = 822781\ in Scala - -lemma \- 805167 XOR (767063 :: integer) = - 523642\ - by normalization - -test_code \- 805167 XOR (767063 :: integer) = - 523642\ in Scala - -lemma \473514 XOR (- 314527 :: integer) = - 259381\ - by normalization - -test_code \473514 XOR (- 314527 :: integer) = - 259381\ in Scala - -lemma \- 805167 XOR (- 314527 :: integer) = 558512\ - by normalization - -test_code \- 805167 XOR (- 314527 :: integer) = 558512\ in Scala - -lemma \NOT (473513 :: integer) = - 473514\ - by normalization - -test_code \NOT (473513 :: integer) = - 473514\ in Scala - -lemma \NOT (- 805167 :: integer) = 805166\ - by normalization - -test_code \NOT (- 805167 :: integer) = 805166\ in Scala - -lemma \(mask 39 :: integer) = 549755813887\ - by normalization - -test_code \(mask 39 :: integer) = 549755813887\ in Scala - -lemma \set_bit 15 (473514 :: integer) = 506282\ - by normalization - -test_code \set_bit 15 (473514 :: integer) = 506282\ in Scala - -lemma \set_bit 11 (- 805167 :: integer) = - 803119\ - by normalization - -test_code \set_bit 11 (- 805167 :: integer) = - 803119\ in Scala - -lemma \unset_bit 13 (473514 :: integer) = 465322\ - by normalization - -test_code \unset_bit 13 (473514 :: integer) = 465322\ in Scala - -lemma \unset_bit 12 (- 805167 :: integer) = - 809263\ - by normalization - -test_code \unset_bit 12 (- 805167 :: integer) = - 809263\ in Scala - -lemma \flip_bit 15 (473514 :: integer) = 506282\ - by normalization - -test_code \flip_bit 15 (473514 :: integer) = 506282\ in Scala - -lemma \flip_bit 12 (- 805167 :: integer) = - 809263\ - by normalization - -test_code \flip_bit 12 (- 805167 :: integer) = - 809263\ in Scala - -lemma \push_bit 12 (473514 :: integer) = 1939513344\ - by normalization - -test_code \push_bit 12 (473514 :: integer) = 1939513344\ in Scala - -lemma \push_bit 12 (- 805167 :: integer) = - 3297964032\ - by normalization - -test_code \push_bit 12 (- 805167 :: integer) = - 3297964032\ in Scala - -lemma \drop_bit 12 (473514 :: integer) = 115\ - by normalization - -test_code \drop_bit 12 (473514 :: integer) = 115\ in Scala - -lemma \drop_bit 12 (- 805167 :: integer) = - 197\ - by normalization - -test_code \drop_bit 12 (- 805167 :: integer) = - 197\ in Scala - -lemma \take_bit 12 (473514 :: integer) = 2474\ - by normalization - -test_code \take_bit 12 (473514 :: integer) = 2474\ in Scala - -lemma \take_bit 12 (- 805167 :: integer) = 1745\ - by normalization - -test_code \take_bit 12 (- 805167 :: integer) = 1745\ in Scala - -lemma \signed_take_bit 12 (473514 :: integer) = - 1622\ - by normalization - -test_code \signed_take_bit 12 (473514 :: integer) = - 1622\ in Scala - -lemma \signed_take_bit 12 (- 805167 :: integer) = - 2351\ - by normalization - -test_code \signed_take_bit 12 (- 805167 :: integer) = - 2351\ in Scala - end diff -r fa0bafdc0fc6 -r f0ae2acbefd5 src/HOL/Codegenerator_Test/Generate_Target_Bit_Operations.thy --- 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 \Checking the index maximum for \\PolyML\\ + +definition \check_max = ()\ + +definition \anchor = (Code_Target_Bit_Shifts.drop_bit, check_max)\ + +code_printing + code_module Check_Max \ + (SML) \ +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; +\ + | constant check_max \ + (SML) "check'_max Bit'_Shifts.word'_max'_index" + +test_code \snd anchor = ()\ in PolyML + end diff -r fa0bafdc0fc6 -r f0ae2acbefd5 src/HOL/Library/Code_Bit_Shifts_for_Arithmetic.thy --- /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 \Rewrite arithmetic operations to bit-shifts if feasible\ + +theory Code_Bit_Shifts_for_Arithmetic + imports Main +begin + +context semiring_bit_operations +begin + +context + includes bit_operations_syntax +begin + +lemma [code_unfold]: + \of_bool (odd a) = a AND 1\ + by (simp add: and_one_eq mod2_eq_if) + +lemma [code_unfold]: + \even a \ a AND 1 = 0\ + by (simp add: and_one_eq mod2_eq_if) + +lemma [code_unfold]: + \2 * a = push_bit 1 a\ + by (simp add: ac_simps) + +lemma [code_unfold]: + \a * 2 = push_bit 1 a\ + by simp + +lemma [code_unfold]: + \2 ^ n * a = push_bit n a\ + by (simp add: push_bit_eq_mult ac_simps) + +lemma [code_unfold]: + \a * 2 ^ n = push_bit n a\ + by (simp add: push_bit_eq_mult) + +lemma [code_unfold]: + \a div 2 = drop_bit 1 a\ + by (simp add: drop_bit_eq_div) + +lemma [code_unfold]: + \a div 2 ^ n = drop_bit n a\ + by (simp add: drop_bit_eq_div) + +lemma [code_unfold]: + \a mod 2 = take_bit 1 a\ + by (simp add: take_bit_eq_mod) + +lemma [code_unfold]: + \a mod 2 ^ n = take_bit n a\ + by (simp add: take_bit_eq_mod) + +end + +end + +end diff -r fa0bafdc0fc6 -r f0ae2acbefd5 src/HOL/Library/Code_Target_Bit_Shifts.thy --- 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; diff -r fa0bafdc0fc6 -r f0ae2acbefd5 src/HOL/Library/Complete_Partial_Order2.thy --- 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 (\) Y" -by(auto intro: chainI) + by(auto intro: chainI) lemma fun_lub_apply: "\Sup. fun_lub Sup Y x = Sup ((\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 {} = (\_. 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 ((\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 \ 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 \ 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 \ 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 (\)) (mk_less (fun_ord (\)))" 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 (\) Y \ Sup Y \ x \ (\y\Y. y \ 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 (\) A" @@ -152,11 +152,9 @@ proof(rule ccpo_Sup_least) fix y assume "y \ (\x. f x x) ` Y" - then obtain x where "x \ Y" and "y = f x x" by blast note this(2) - also from chain2[OF \x \ Y\] have "\ \ \(f x ` Y)" - by(rule ccpo_Sup_upper)(simp add: \x \ Y\) - also have "\ \ ?lhs" by(rule ccpo_Sup_upper[OF chain1])(simp add: \x \ Y\) - finally show "y \ ?lhs" . + then obtain x where "x \ Y" and "y = f x x" by blast + then show "y \ ?lhs" + by (metis (no_types, lifting) chain1 chain2 imageI ccpo_Sup_upper order.trans) qed qed @@ -180,6 +178,7 @@ finally show "x \ \" . qed + lemma swap_Sup: fixes le_b (infix \\\ 60) assumes Y: "Complete_Partial_Order.chain (\) Y" @@ -222,11 +221,10 @@ proof(rule ccpo_Sup_least) fix x' assume "x' \ (\f. f x) ` Z" - then obtain f where "f \ Z" "x' = f x" by blast note this(2) - also have "f x \ f y" using \f \ Z\ \x \ y\ by(rule monotoneD[OF mono]) - also have "f y \ ?rhs" using chain3 - by(rule ccpo_Sup_upper)(simp add: \f \ Z\) - finally show "x' \ ?rhs" . + then obtain f where "f \ Z" "x' = f x" by blast + then show "x' \ ?rhs" + by (metis (mono_tags, lifting) \x \ y\ chain3 imageI ccpo_Sup_upper + order_trans mono monotoneD) qed qed @@ -239,11 +237,10 @@ proof(rule ccpo_Sup_least) fix x' assume "x' \ f ` Y" - then obtain y where "y \ Y" "x' = f y" by blast note this(2) - also have "f y \ \((\f. f y) ` Z)" using chain3 - by(rule ccpo_Sup_upper)(simp add: \f \ Z\) - also have "\ \ ?rhs" using chain4 by(rule ccpo_Sup_upper)(simp add: \y \ Y\) - finally show "x' \ ?rhs" . + then obtain y where "y \ Y" "x' = f y" by blast + then show "x' \ ?rhs" + by (metis (mono_tags, lifting) \f \ Z\ chain3 chain4 imageI local.ccpo_Sup_upper + order.trans) qed finally show "x \ ?rhs" . qed @@ -257,12 +254,10 @@ proof(rule ccpo_Sup_least) fix x' assume "x' \ (\f. f y) ` Z" - then obtain f where "f \ Z" "x' = f y" by blast note this(2) - also have "f y \ \(f ` Y)" using chain1[OF \f \ Z\] - by(rule ccpo_Sup_upper)(simp add: \y \ Y\) - also have "\ \ ?lhs" using chain2 - by(rule ccpo_Sup_upper)(simp add: \f \ Z\) - finally show "x' \ ?lhs" . + then obtain f where "f \ Z" "x' = f y" by blast + then show "x' \ ?lhs" + by (metis (mono_tags, lifting) \y \ Y\ ccpo_Sup_below_iff chain1 chain2 imageI + ccpo_Sup_upper) qed finally show "x \ ?lhs" . qed @@ -411,47 +406,47 @@ declare if_mono[simp] lemma monotone_id' [cont_intro]: "monotone ord ord (\x. x)" -by(simp add: monotone_def) + by(simp add: monotone_def) lemma monotone_applyI: "monotone orda ordb F \ monotone (fun_ord orda) ordb (\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]: "\ monotone (fun_ord orda) (fun_ord ordb) F; monotone (fun_ord orda) (fun_ord ordb) G \ \ monotone (fun_ord orda) (fun_ord ordb) (\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) (\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 \ (\x. monotone orda ordb (\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 (\) (\_. c)" -by(rule monotoneI) simp + by(rule monotoneI) simp end lemma transp_le [cont_intro, simp]: "class.preorder ord (mk_less ord) \ 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?]: "(\Y. \ Complete_Partial_Order.chain orda Y; Y \ {} \ \ f (luba Y) = lubb (f ` Y)) \ cont luba orda lubb ordb f" -unfolding cont_def by blast + unfolding cont_def by blast lemma contD: "\ cont luba orda lubb ordb f; Complete_Partial_Order.chain orda Y; Y \ {} \ \ f (luba Y) = lubb (f ` Y)" -unfolding cont_def by blast + unfolding cont_def by blast lemma cont_id [simp, cont_intro]: "\Sup. cont Sup ord Sup ord id" -by(rule contI) simp + by(rule contI) simp lemma cont_id' [simp, cont_intro]: "\Sup. cont Sup ord Sup ord (\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 (\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 (\f. f t)" -by(simp add: cont_def fun_lub_apply) + by(simp add: cont_def fun_lub_apply) lemma cont_if [cont_intro]: "\ cont luba orda lubb ordb f; cont luba orda lubb ordb g \ \ cont luba orda lubb ordb (\x. if c then f x else g x)" -by(cases c) simp_all + by(cases c) simp_all lemma mcontI [intro?]: - "\ monotone orda ordb f; cont luba orda lubb ordb f \ \ mcont luba orda lubb ordb f" -by(simp add: mcont_def) + "\ monotone orda ordb f; cont luba orda lubb ordb f \ \ mcont luba orda lubb ordb f" + by(simp add: mcont_def) lemma mcont_mono: "mcont luba orda lubb ordb f \ monotone orda ordb f" -by(simp add: mcont_def) + by(simp add: mcont_def) lemma mcont_cont [simp]: "mcont luba orda lubb ordb f \ cont luba orda lubb ordb f" -by(simp add: mcont_def) + by(simp add: mcont_def) lemma mcont_monoD: "\ mcont luba orda lubb ordb f; orda x y \ \ ordb (f x) (f y)" -by(auto simp add: mcont_def dest: monotoneD) + by(auto simp add: mcont_def dest: monotoneD) lemma mcont_contD: "\ mcont luba orda lubb ordb f; Complete_Partial_Order.chain orda Y; Y \ {} \ \ 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 (\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 (\x. x)" -by(simp add: mcont_def monotone_id') + by(simp add: mcont_def monotone_id') lemma mcont_applyI: "mcont luba orda lubb ordb (\x. F x) \ mcont (fun_lub luba) (fun_ord orda) lubb ordb (\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]: "\ mcont luba orda lubb ordb (\x. f x); mcont luba orda lubb ordb (\x. g x) \ \ mcont luba orda lubb ordb (\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 \ (\x. cont luba orda lubb ordb (\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 \ (\x. mcont luba orda lubb ordb (\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 (\) (\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 (\) (\x. c)" -by(simp add: mcont_def) + by(simp add: mcont_def) lemma cont_apply: assumes 2: "\x. cont lubb ordb Sup (\) (\y. f x y)" - and t: "cont luba orda lubb ordb (\x. t x)" - and 1: "\y. cont luba orda Sup (\) (\x. f x y)" - and mono: "monotone orda ordb (\x. t x)" - and mono2: "\x. monotone ordb (\) (\y. f x y)" - and mono1: "\y. monotone orda (\) (\x. f x y)" + and t: "cont luba orda lubb ordb (\x. t x)" + and 1: "\y. cont luba orda Sup (\) (\x. f x y)" + and mono: "monotone orda ordb (\x. t x)" + and mono2: "\x. monotone ordb (\) (\y. f x y)" + and mono1: "\y. monotone orda (\) (\x. f x y)" shows "cont luba orda Sup (\) (\x. f x (t x))" proof fix Y @@ -561,16 +556,16 @@ \y. mcont lub ord Sup (\) (\x. f x y); mcont lub ord lub' ord' (\y. t y) \ \ mcont lub ord Sup (\) (\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: "\mcont lub' ord' Sup (\) (\x. f x); mcont lub ord lub' ord' (\x. t x)\ \ mcont lub ord Sup (\) (\x. f (t x))" -by(rule mcont2mcont'[OF _ mcont_const]) + by(rule mcont2mcont'[OF _ mcont_const]) context fixes ord :: "'b \ 'b \ bool" (infix \\\ 60) - and lub :: "'b set \ 'b" (\\\) + and lub :: "'b set \ 'b" (\\\) begin lemma cont_fun_lub_Sup: @@ -818,42 +813,42 @@ lemma admissible_disj' [simp, cont_intro]: "\ class.ccpo lub ord (mk_less ord); ccpo.admissible lub ord P; ccpo.admissible lub ord Q \ \ ccpo.admissible lub ord (\x. P x \ Q x)" -by(rule ccpo.admissible_disj) + by(rule ccpo.admissible_disj) lemma admissible_imp' [cont_intro]: "\ class.ccpo lub ord (mk_less ord); ccpo.admissible lub ord (\x. \ P x); ccpo.admissible lub ord (\x. Q x) \ \ ccpo.admissible lub ord (\x. P x \ 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 \ ccpo.admissible lub ord (\x. P x)) \ ccpo.admissible lub ord (\x. Q \ 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 (\) (\A. x \ A)" -by(rule ccpo.admissibleI) auto + by(rule ccpo.admissibleI) auto lemma admissible_eqI: assumes f: "cont luba orda lub ord (\x. f x)" - and g: "cont luba orda lub ord (\x. g x)" + and g: "cont luba orda lub ord (\x. g x)" shows "ccpo.admissible luba orda (\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]: "\ mcont luba orda lub ord (\x. f x); mcont luba orda lub ord (\x. g x) \ \ ccpo.admissible luba orda (\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]: "\ ccpo.admissible lub ord (\x. P x \ Q x); ccpo.admissible lub ord (\x. Q x \ P x) \ \ ccpo.admissible lub ord (\x. P x \ 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 (\_. lub {})" and step: "\f'. \ P (U f'); le_fun (U f') (U f) \ \ 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 \\<^term>\(=)\ as order\ definition lub_singleton :: "('a set \ 'a) \ bool" -where "lub_singleton lub \ (\a. lub {a} = a)" + where "lub_singleton lub \ (\a. lub {a} = a)" definition the_Sup :: "'a set \ 'a" -where "the_Sup A = (THE a. a \ A)" + where "the_Sup A = (THE a. a \ 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]: "\ class.preorder ord (mk_less ord); lub_singleton lub \ \ 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 \ccpo for products\ definition prod_lub :: "('a set \ 'a) \ ('b set \ 'b) \ ('a \ 'b) set \ 'a \ '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]: "\ lub_singleton luba; lub_singleton lubb \ \ 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: "\a. monotone ordb ordc (\b. f (a, b))" - and mono1: "\b. monotone orda ordc (\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: "\b. monotone orda ordc (\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 (\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 (\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) \ \ 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 (\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 \ (\a. monotone ordb ordc (\b. f (a, b))) \ (\b. monotone orda ordc (\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) \ (\a. monotone ordb ordc (f a)) \ (\b. monotone orda ordc (\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 (\x. (case_prod f x) y) \ monotone orda ordb (case_prod (\a b. f a b y))" -by(simp add: monotone_def) + by(simp add: monotone_def) lemma monotone_case_prod_applyD: "monotone orda ordb (\x. (case_prod f x) y) \ monotone orda ordb (case_prod (\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 (\a b. f a b y)) \ monotone orda ordb (\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 (\x. (case_prod f x) y) \ cont luba orda lubb ordb (case_prod (\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 (\a b. f a b y)) \ cont luba orda lubb ordb (\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 (\x. (case_prod f x) y) \ cont luba orda lubb ordb (case_prod (\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 (\x. (case_prod f x) y) \ @@ -1307,13 +1302,8 @@ and t: "monotone orda ordb (\x. t x)" and t': "monotone orda ordc (\x. t' x)" shows "monotone orda leq (\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]: "\ 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) \ \ 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: "\ monotone (rel_prod orda ordb) leq (case_prod f); @@ -1330,39 +1320,39 @@ class.preorder ordb (mk_less ordb); lub_singleton lubb \ \ cont (prod_lub luba lubb) (rel_prod orda ordb) lub leq (case_prod f) \ (\x. cont lubb ordb lub leq (\y. f x y)) \ (\y. cont luba orda lub leq (\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]: "\ class.preorder orda (mk_less orda); lub_singleton luba; class.preorder ordb (mk_less ordb); lub_singleton lubb \ \ mcont (prod_lub luba lubb) (rel_prod orda ordb) lub leq (case_prod f) \ (\x. mcont lubb ordb lub leq (\y. f x y)) \ (\y. mcont luba orda lub leq (\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 "\x y. monotone orda ordb (\f. pair f x y)" shows "monotone orda ordb (\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 \Complete lattices as ccpo\ context complete_lattice begin lemma complete_lattice_ccpo: "class.ccpo Sup (\) (<)" -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 (\) (mk_less (\))" -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 (\) 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 (\) 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 (\) (\x. f x)" - and g: "monotone ord (\) (\x. g x)" + and g: "monotone ord (\) (\x. g x)" shows "monotone ord (\) (\x. f x \ 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 (\) (\_. 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 (\) (\x. f x)" - and g: "monotone ord (\) (\x. g x)" + and g: "monotone ord (\) (\x. g x)" shows "monotone ord (\) (\x. f x \ 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 \ {}" @@ -1408,16 +1398,16 @@ qed lemma mcont_sup1: "mcont Sup (\) Sup (\) (\y. x \ 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 (\) Sup (\) (\x. x \ y)" -by(subst sup_commute)(rule mcont_sup1) + by(subst sup_commute)(rule mcont_sup1) lemma mcont2mcont_sup [cont_intro, simp]: "\ mcont lub ord Sup (\) (\x. f x); mcont lub ord Sup (\) (\x. g x) \ \ mcont lub ord Sup (\) (\x. f x \ 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 (\) Sup (\) (\y. x \ 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 (\) Sup (\) (\x. x \ 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]: "\ mcont lub ord Sup (\) (\x. f x); mcont lub ord Sup (\) (\x. g x) \ \ mcont lub ord Sup (\) (\x. f x \ 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 "(\) :: _ :: complete_lattice \ _" Sup -by(rule complete_lattice_partial_function_definitions) + by(rule complete_lattice_partial_function_definitions) declaration \Partial_Function.init "lfp" \<^term>\lfp.fixp_fun\ \<^term>\lfp.mono_body\ @{thm lfp.fixp_rule_uc} @{thm lfp.fixp_induct_uc} NONE\ interpretation gfp: partial_function_definitions "(\) :: _ :: complete_lattice \ _" Inf -by(rule complete_lattice_partial_function_definitions_dual) + by(rule complete_lattice_partial_function_definitions_dual) declaration \Partial_Function.init "gfp" \<^term>\gfp.fixp_fun\ \<^term>\gfp.mono_body\ @{thm gfp.fixp_rule_uc} @{thm gfp.fixp_induct_uc} NONE\ lemma insert_mono [partial_function_mono]: - "monotone (fun_ord (\)) (\) A \ monotone (fun_ord (\)) (\) (\y. insert x (A y))" -by(rule monotoneI)(auto simp add: fun_ord_def dest: monotoneD) + "monotone (fun_ord (\)) (\) A \ monotone (fun_ord (\)) (\) (\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 (\) (\) (insert x)" -by(rule monotoneI) blast + by(rule monotoneI) blast lemma mcont2mcont_insert[THEN lfp.mcont2mcont, cont_intro, simp]: shows mcont_insert: "mcont Union (\) Union (\) (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 (\) (\) ((`) f)" -by(rule monotoneI) blast + by(rule monotoneI) blast lemma cont_image: "cont Union (\) Union (\) ((`) f)" -by(rule contI)(auto) + by(rule contI)(auto) lemma mcont2mcont_image [THEN lfp.mcont2mcont, cont_intro, simp]: shows mcont_image: "mcont Union (\) Union (\) ((`) 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 (\) f \ monotone ord (\) (\x. \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 (\) 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 \ mcont lub ord luba orda (\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: "\ monotone ord orda f; monotone ord ordb g \ \ monotone ord (rel_prod orda ordb) (\x. (f x, g x))" -by(simp add: monotone_def) + by(simp add: monotone_def) lemma cont_Pair: "\ cont lub ord luba orda f; cont lub ord lubb ordb g \ \ cont lub ord (prod_lub luba lubb) (rel_prod orda ordb) (\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: "\ mcont lub ord luba orda f; mcont lub ord lubb ordb g \ \ mcont lub ord (prod_lub luba lubb) (rel_prod orda ordb) (\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 \Specialised versions of @{thm [source] mcont_call} for admissibility proofs for parallel fixpoint inductions\ 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] diff -r fa0bafdc0fc6 -r f0ae2acbefd5 src/HOL/Library/Extended_Nat.thy --- 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 \Multiplication\ @@ -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 \ 0 \ b \ 0 \ a * b \ 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 \ enat n \ numeral m \ n" -by (auto simp: numeral_eq_enat) + by (auto simp: numeral_eq_enat) lemma numeral_less_enat_iff[simp]: shows "numeral m < enat n \ numeral m < n" -by (auto simp: numeral_eq_enat) + by (auto simp: numeral_eq_enat) lemma enat_ord_code [code]: "enat m \ enat n \ m \ n" @@ -472,17 +452,15 @@ by(cases x y rule: enat.exhaust[case_product enat.exhaust]) simp_all lemma chain_incr: "\i. \j. Y i < Y j \ \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 \ {}" 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 \ {..enat n}" using le_fin by fastforce - also have "\ \ enat ` {..n}" - apply (rule subsetI) - subgoal for x by (cases x) auto - done - finally show "A \ enat ` {..n}" . + have "A \ enat ` {..n}" + using enat_ile le_fin by fastforce + then show "A \ enat ` {..n}" . qed subsection \Cancellation simprocs\ lemma add_diff_cancel_enat[simp]: "x \ \ \ 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 \ a = (\::enat) \ 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 = \ \ m=\ \ n=\" -using enat_add_left_cancel by fastforce + using enat_add_left_cancel by fastforce ML \ structure Cancel_Enat_Common = @@ -605,32 +577,21 @@ subsection \Well-ordering\ lemma less_enatE: - "[| n < enat m; !!k. n = enat k ==> k < m ==> P |] ==> P" -by (induct n) auto + "\n < enat m; \k. \n = enat k; k < m\ \ P\ \ P" + using enat_iless enat_ord_simps(2) by blast lemma less_infinityE: - "[| n < \; !!k. n = enat k ==> P |] ==> P" -by (induct n) auto + "\n < \; \k. n = enat k \ P\ \ P" + by auto lemma enat_less_induct: - assumes prem: "\n. \m::enat. m < n \ P m \ P n" shows "P n" + assumes "\n. \m::enat. m < n \ P m \ P n" + shows "P n" proof - - have P_enat: "\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 \" - 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 diff -r fa0bafdc0fc6 -r f0ae2acbefd5 src/HOL/Library/Extended_Nonnegative_Real.thy --- 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 \ bot \ Limsup F (\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 \ bot \ Liminf F (\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 \ bot \ Liminf F (\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 \ '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 "\ (lfp f) \ lfp g" unfolding sup_continuous_lfp[OF f] - by (subst \[THEN sup_continuousD]) - (auto intro!: mono_funpow sup_continuous_mono[OF f] SUP_least) - + by (simp add: SUP_least \[THEN sup_continuousD] mf mono_funpow) show "lfp g \ \ (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\{n..}. enn2ereal (y x)) = (SUP x\{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 (\x. INF n. sup 0 (SUP i\{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 "\x y. \rel_fun (=) pcr_ennreal x y; + pcr_ennreal (INF n::nat. max 0 (Sup (x ` {n..}))) (INF n. Sup (y ` {n..}))\ + \ 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]: "(\i. i \ I \ 0 \ f i) \ (\i\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 \Cancellation simprocs\ @@ -654,7 +650,7 @@ fixes a b c :: ennreal shows "a - b \ a - c \ a < top \ b \ a \ c \ a \ c \ 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 \ b < top \ 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 \ 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 \ 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 \ 0 < a \ 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 \ top \ 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 \ q \ 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 \ (n \ 0 \ (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 \ 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 \ x \ 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 \ (a = b \ c \ 0)" -proof (cases "0 \ 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: "(\e::real. y < top \ 0 < e \ x \ y + ennreal e) \ x \ y" @@ -1166,13 +1153,13 @@ lemma enn2ereal_Iio: "enn2ereal -` {.. 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 \ 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..} \ {..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 _ _ "\_. 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 \ {0..} \ {..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 (\x. e2ennreal (f x))" @@ -1370,7 +1355,7 @@ unfolding sums_def by (simp add: always_eventually sum_nonneg) lemma suminf_enn2ereal[simp]: "(\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 \ ennreal" shows "(\i. g i \ f i) \ suminf f \ top \ suminf g \ top \ (\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 \ {} \ \f::nat \ ennreal. incseq f \ range f \ A \ Sup A = (SUP i. f i)" @@ -1605,7 +1590,7 @@ have "f (SUP i \ I. g i) = (SUP i \ range M. f i)" unfolding eq sup_continuousD[OF f \mono M\] by (simp add: image_comp) also have "\ \ (SUP i \ 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 \ I. g i) \ (SUP i \ I. f (g i))" . qed @@ -1633,8 +1618,9 @@ (* Contributed by Dominique Unruh *) lemma isCont_ennreal[simp]: \isCont ennreal x\ - 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]: \isCont ennreal_of_enat x\ @@ -1672,12 +1658,8 @@ define s where \s = {x}\ have \open s\ using False open_enat_iff s_def by blast - moreover have \x \ s\ - using s_def by auto - moreover have \ennreal_of_enat z \ t\ if \z \ s\ for z - using asm s_def that by blast - ultimately show \\s. open s \ x \ s \ (\z\s. ennreal_of_enat z \ t)\ - by auto + then show \\s. open s \ x \ s \ (\z\s. ennreal_of_enat z \ t)\ + 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 \ A. f i)" + assumes "x = (INF i \ A. f i)" assumes "x \ \" shows "\i \ A. f i < x + e" -proof - - have "(INF i \ A. f i) < x + e" - unfolding INF[symmetric] using \0 \x \ \\ 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: "(\a::ennreal. 0 < a \ a < 1 \ a * z \ y) \ z \ y" - apply (subst SUP_mult_right_ennreal[of "\x. x" "{0 <..< 1}" z, simplified]) - apply (auto intro: SUP_least) - done + using SUP_mult_right_ennreal[of "\x. x" "{0 <..< 1}" z] + by (smt (verit) SUP_least Sup_greaterThanLessThan greaterThanLessThan_iff + image_ident mult_1 zero_less_one) lemma suminf_ennreal2: "(\i. 0 \ f i) \ summable f \ (\i. ennreal (f i)) = ennreal (\i. f i)" @@ -1784,11 +1761,8 @@ lemma ennreal_tendsto_top_eq_at_top: "((\z. ennreal (f z)) \ top) F \ (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 :: "_ \ ennreal" @@ -1874,10 +1848,7 @@ lemma add_diff_eq_iff_ennreal[simp]: fixes x y :: ennreal shows "x + (y - x) = y \ x \ y" -proof - assume *: "x + (y - x) = y" show "x \ 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 \ 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 \ x < top \ 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) \ (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) \ (b \ top \ b \ 0 \ b = a)" by (cases a ; cases b; cases "b = 0") (auto simp: ennreal_top_divide divide_ennreal split: if_split_asm) diff -r fa0bafdc0fc6 -r f0ae2acbefd5 src/HOL/Library/Float.thy --- 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 \ float \ sgn x \ 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 \ float \ x / 2^d \ 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 \ int \ float" is "\(m::int) (e::int). m * 2 powr e" @@ -383,11 +383,10 @@ by (auto simp: float_def) with \x \ 0\ int_cancel_factors[of 2 m] obtain k i where "m = k * 2 ^ i" "\ 2 dvd k" by auto - with \\ 2 dvd k\ 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 \\ 2 dvd k\ x have "x = real_of_int k * 2 powr real_of_int (e + int i) \ 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 \x > 0\ \y > 0\ 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 \1 < p\, THEN iffD2] have "floor ?r = (if i \ 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 \ 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 \ x" "0 < y" "x \ y" @@ -2232,7 +2229,7 @@ by transfer (rule real_divl_pos_less1_bound) lemma float_divr: "real_of_float x / real_of_float y \ 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" diff -r fa0bafdc0fc6 -r f0ae2acbefd5 src/HOL/Library/ListVector.thy --- 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 \Lists as vectors\ theory ListVector -imports Main + imports Main begin text\\noindent @@ -13,19 +13,19 @@ text\Multiplication with a scalar:\ abbreviation scale :: "('a::times) \ 'a list \ 'a list" (infix \*\<^sub>s\ 70) -where "x *\<^sub>s xs \ map ((*) x) xs" + where "x *\<^sub>s xs \ 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 \\+\ and \-\\ fun zipwith0 :: "('a::zero \ 'b::zero \ 'c) \ 'a list \ 'b list \ '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 "\xs,ys\ = (\(x,y) \ zip xs ys. x*y)" lemma iprod_Nil[simp]: "\[],ys\ = 0" -by(simp add: iprod_def) + by(simp add: iprod_def) lemma iprod_Nil2[simp]: "\xs,[]\ = 0" -by(simp add: iprod_def) + by(simp add: iprod_def) lemma iprod_Cons[simp]: "\x#xs,y#ys\ = x*y + \xs,ys\" -by(simp add: iprod_def) + by(simp add: iprod_def) lemma iprod0_if_coeffs0: "\c\set cs. c = 0 \ \cs,xs\ = 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]: "\-xs,ys\ = -\xs,ys\" -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: "\xs + ys,zs\ = \xs,zs\ + \ys,zs\" -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: "\xs - ys, zs\ = \xs,zs\ - \ys,zs\" -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: "\x *\<^sub>s xs, ys\ = x * \xs,ys\" -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 diff -r fa0bafdc0fc6 -r f0ae2acbefd5 src/HOL/Library/Poly_Mapping.thy --- 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 \ 'a :: mult_zero" assumes "finite {a. f a \ 0}" shows "finite {a. g a * f a \ 0}" -proof - - have "{a. g a * f a \ 0} \ {a. f a \ 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 \ 'a :: mult_zero" assumes "finite {a. f a \ 0}" shows "finite {a. f a * g a \ 0}" -proof - - have "{a. f a * g a \ 0} \ {a. f a \ 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 \ 'b::semiring_0" @@ -227,10 +221,7 @@ typedef (overloaded) ('a, 'b) poly_mapping (\(_ \\<^sub>0 /_)\ [1, 0] 0) = "{f :: 'a \ 'b::zero. finite {x. f x \ 0}}" morphisms lookup Abs_poly_mapping -proof - - have "(\_::'a. (0 :: 'b)) \ ?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 \ 'b) \ ('a \ 'b) \ 'a::monoid_add \ 'b::semiring_0" where @@ -455,8 +444,9 @@ proof - let ?C = "{a. f a \ 0} \ {b. g b \ 0}" from fin_f fin_g have "finite ?C" by blast - moreover have "{a. \b. (f a * g b when k = a + b) \ 0} \ - {b. \a. (f a * g b when k = a + b) \ 0} \ {a. f a \ 0} \ {b. g b \ 0}" + moreover + have "{a. \b. (f a * g b when k = a + b) \ 0} \ + {b. \a. (f a * g b when k = a + b) \ 0} \ {a. f a \ 0} \ {b. g b \ 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 \ k' \ 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 \ of_nat" @@ -923,14 +909,7 @@ fix f g h :: "'a \ 'b" assume *: "less_fun f g \ f = g" have "less_fun (\k. h k + f k) (\k. h k + g k)" if "less_fun f g" - proof - - from that obtain k where "f k < g k" "(\k'. k' < k \ f k' = g k')" - by (blast elim!: less_funE) - then have "h k + f k < h k + g k" "(\k'. k' < k \ 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 (\k. h k + f k) (\k. h k + g k) \ (\k. h k + f k) = (\k. h k + g k)" by (auto simp: fun_eq_iff) qed @@ -986,7 +965,7 @@ have "Set.range f - {0} \ f ` {x. f x \ 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 \ (keys s) = (lookup s x \ 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 \ 'd" and p :: "'a \ 'c" assume "finite {x. p x \ 0}" hence "finite (f ` {y. p (f y) \ 0})" - by(rule finite_subset[rotated]) auto + by (simp add: rev_finite_subset subset_eq) thus "finite {x. (p \ f) x \ 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.. 0 | Some v \ 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 \ snd ` set xs" @@ -1552,15 +1531,10 @@ proof - from assms obtain k where *: "lookup m k = v" "v \ 0" by transfer blast - from * have "k \ keys m" + then have "k \ keys m" by (simp add: in_keys_iff) - then show ?thesis - proof (rule poly_mapping_size_estimation) - from assms * have "y \ g (lookup m k)" - by simp - then show "y \ 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 \ 0" -proof - - let ?f = "\x. if x = a then 1 else (0::int)" - have "?f \ (\x. 0::int)" - by (auto simp: fun_eq_iff) - then have "Poly_Mapping.lookup (Abs_poly_mapping ?f) \ Poly_Mapping.lookup (Abs_poly_mapping (\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 \ ('a \\<^sub>0 int) \ ('a \\<^sub>0 int)" where "frag_cmul c a = Abs_poly_mapping (\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 \ 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) diff -r fa0bafdc0fc6 -r f0ae2acbefd5 src/HOL/Library/Signed_Division.thy --- 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 \ 0 \ ((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 \ 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 \ 0 \ ((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: \a sdiv b \ {- \a\..\a\}\ for a b :: int @@ -178,9 +170,8 @@ "\ 0 \ a; b < 0 \ \ 0 \ (a :: int) smod b" "\ a \ 0; b < 0 \ \ (a :: int) smod b \ 0" "\ a \ 0; b < 0 \ \ b \ (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: "\ 0 \ (a :: int); 0 \ b \ \ a smod b = a mod b" diff -r fa0bafdc0fc6 -r f0ae2acbefd5 src/HOL/Library/Suc_Notation.thy --- /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 \Suc\ terms. Just notation. Use standard numerals for large numbers. +*) + +theory Suc_Notation +imports Main +begin + +text \Nested \Suc\ terms of depth \2 \ n \ 9\ are abbreviated with new notations \Suc\<^sup>n\:\ + +abbreviation (input) Suc2 where "Suc2 n \ Suc (Suc n)" +abbreviation (input) Suc3 where "Suc3 n \ Suc (Suc2 n)" +abbreviation (input) Suc4 where "Suc4 n \ Suc (Suc3 n)" +abbreviation (input) Suc5 where "Suc5 n \ Suc (Suc4 n)" +abbreviation (input) Suc6 where "Suc6 n \ Suc (Suc5 n)" +abbreviation (input) Suc7 where "Suc7 n \ Suc (Suc6 n)" +abbreviation (input) Suc8 where "Suc8 n \ Suc (Suc7 n)" +abbreviation (input) Suc9 where "Suc9 n \ 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 \Beyond 9, the syntax \Suc\<^bsup>n\<^esup>\ kicks in:\ + +syntax + "_Suc_tower" :: "num_token \ nat \ nat" ("Suc\<^bsup>_\<^esup>") + +parse_translation \ + let + fun mk_sucs_aux 0 t = t + | mk_sucs_aux n t = mk_sucs_aux (n - 1) (\<^const>\Suc\ $ t) + fun mk_sucs n = Abs("n", \<^typ>\nat\, mk_sucs_aux n (Bound 0)) + + fun Suc_tr [Free (str, _)] = mk_sucs (the (Int.fromString str)) + + in [(\<^syntax_const>\_Suc_tower\, K Suc_tr)] end +\ + +print_translation \ + let + val digit_consts = + [\<^const_syntax>\Suc2\, \<^const_syntax>\Suc3\, \<^const_syntax>\Suc4\, \<^const_syntax>\Suc5\, + \<^const_syntax>\Suc6\, \<^const_syntax>\Suc7\, \<^const_syntax>\Suc8\, \<^const_syntax>\Suc9\] + 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>\Suc\, _) $ 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>\_Suc_tower\, 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>\Suc\, K Suc_tr')] + end +\ + +(* Tests + +ML \ +local + fun mk 0 = \<^term>\x :: nat\ + | mk n = \<^const>\Suc\ $ 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 +\ + +(* 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 \ Suc\<^sup>3 n = n+3 \ Suc\<^sup>4 n = n+4 \ Suc\<^sup>5 n = n+5 + \ Suc\<^sup>6 n = n+6 \ Suc\<^sup>7 n = n+7 \ Suc\<^sup>8 n = n+8 \ Suc\<^sup>9 n = n+9" +by simp + +lemma "Suc\<^bsup>10\<^esup> n = n+10 \ Suc\<^bsup>11\<^esup> n = n+11 \ Suc\<^bsup>12\<^esup> n = n+12 \ Suc\<^bsup>13\<^esup> n = n+13 + \ Suc\<^bsup>14\<^esup> n = n+14 \ Suc\<^bsup>15\<^esup> n = n+15 \ Suc\<^bsup>16\<^esup> n = n+16 \ Suc\<^bsup>17\<^esup> n = n+17 + \ Suc\<^bsup>18\<^esup> n = n+18 \ Suc\<^bsup>19\<^esup> n = n+19 \ Suc\<^bsup>20\<^esup> n = n+20" +by simp + +*) + +end \ No newline at end of file diff -r fa0bafdc0fc6 -r f0ae2acbefd5 src/HOL/ROOT --- 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*) diff -r fa0bafdc0fc6 -r f0ae2acbefd5 src/HOL/Tools/BNF/bnf_def.ML --- 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 diff -r fa0bafdc0fc6 -r f0ae2acbefd5 src/HOL/Tools/BNF/bnf_lift.ML --- 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; diff -r fa0bafdc0fc6 -r f0ae2acbefd5 src/HOL/Tools/inductive.ML --- 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 diff -r fa0bafdc0fc6 -r f0ae2acbefd5 src/HOL/Tools/inductive_set.ML --- 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; diff -r fa0bafdc0fc6 -r f0ae2acbefd5 src/Pure/Build/build_schedule.scala --- 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) diff -r fa0bafdc0fc6 -r f0ae2acbefd5 src/Pure/General/mercurial.scala --- 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 diff -r fa0bafdc0fc6 -r f0ae2acbefd5 src/Pure/System/isabelle_system.scala --- 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") {