# HG changeset patch # User haftmann # Date 1737016018 -3600 # Node ID 0b31f0909060172ba48070de1760526458bcdadd # Parent d4eaefc626ec1a0cd3e67a36c4bd11f5fd917ec5 dropped redundant material (left-over from 5e3dd01a9eb2) diff -r d4eaefc626ec -r 0b31f0909060 src/HOL/Codegenerator_Test/Code_Test_GHC.thy --- a/src/HOL/Codegenerator_Test/Code_Test_GHC.thy Thu Jan 16 09:26:57 2025 +0100 +++ b/src/HOL/Codegenerator_Test/Code_Test_GHC.thy Thu Jan 16 09:26:58 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 d4eaefc626ec -r 0b31f0909060 src/HOL/Codegenerator_Test/Code_Test_OCaml.thy --- a/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy Thu Jan 16 09:26:57 2025 +0100 +++ b/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy Thu Jan 16 09:26:58 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 d4eaefc626ec -r 0b31f0909060 src/HOL/Codegenerator_Test/Code_Test_PolyML.thy --- a/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy Thu Jan 16 09:26:57 2025 +0100 +++ b/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy Thu Jan 16 09:26:58 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 d4eaefc626ec -r 0b31f0909060 src/HOL/Codegenerator_Test/Code_Test_Scala.thy --- a/src/HOL/Codegenerator_Test/Code_Test_Scala.thy Thu Jan 16 09:26:57 2025 +0100 +++ b/src/HOL/Codegenerator_Test/Code_Test_Scala.thy Thu Jan 16 09:26:58 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 \