# HG changeset patch # User haftmann # Date 1734985330 -3600 # Node ID e77e8ef5bf9bed0df0b5474be5531c5de73c8e5a # Parent 5af6a5e4343b953dd807a788e819bf8507c1781e explicit tests for target-language bit operations diff -r 5af6a5e4343b -r e77e8ef5bf9b src/HOL/Codegenerator_Test/Code_Test_GHC.thy --- a/src/HOL/Codegenerator_Test/Code_Test_GHC.thy Sun Dec 22 08:46:03 2024 +0100 +++ b/src/HOL/Codegenerator_Test/Code_Test_GHC.thy Mon Dec 23 21:22:10 2024 +0100 @@ -1,10 +1,15 @@ (* Title: HOL/Codegenerator_Test/Code_Test_GHC.thy Author: Andreas Lochbihler, ETH Zurich - -Test case for test_code on GHC + Author: Florian Haftmann, TU Muenchen *) -theory Code_Test_GHC imports "HOL-Library.Code_Test" Code_Lazy_Test begin +theory Code_Test_GHC +imports + "HOL-Library.Code_Test" + Code_Lazy_Test +begin + +text \Test cases for \<^text>\test_code\\ test_code "(14 + 7 * -12 :: integer) = 140 div -2" in GHC @@ -22,4 +27,163 @@ 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 5af6a5e4343b -r e77e8ef5bf9b src/HOL/Codegenerator_Test/Code_Test_OCaml.thy --- a/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy Sun Dec 22 08:46:03 2024 +0100 +++ b/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy Mon Dec 23 21:22:10 2024 +0100 @@ -1,10 +1,15 @@ (* Title: HOL/Codegenerator_Test/Code_Test_OCaml.thy Author: Andreas Lochbihler, ETH Zurich - -Test case for test_code on OCaml + Author: Florian Haftmann, TU Muenchen *) -theory Code_Test_OCaml imports "HOL-Library.Code_Test" Code_Lazy_Test begin +theory Code_Test_OCaml +imports + "HOL-Library.Code_Test" + Code_Lazy_Test +begin + +text \Test cases for \<^text>\test_code\\ test_code "14 + 7 * -12 = (140 div -2 :: integer)" in OCaml @@ -22,4 +27,163 @@ 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 5af6a5e4343b -r e77e8ef5bf9b src/HOL/Codegenerator_Test/Code_Test_PolyML.thy --- a/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy Sun Dec 22 08:46:03 2024 +0100 +++ b/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy Mon Dec 23 21:22:10 2024 +0100 @@ -1,10 +1,15 @@ (* Title: HOL/Codegenerator_Test/Code_Test_PolyML.thy Author: Andreas Lochbihler, ETH Zurich - -Test case for test_code on PolyML + Author: Florian Haftmann, TU Muenchen *) -theory Code_Test_PolyML imports "HOL-Library.Code_Test" Code_Lazy_Test begin +theory Code_Test_PolyML +imports + "HOL-Library.Code_Test" + Code_Lazy_Test +begin + +text \Test cases for \<^text>\test_code\\ test_code "14 + 7 * -12 = (140 div -2 :: integer)" in PolyML @@ -12,4 +17,163 @@ 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 5af6a5e4343b -r e77e8ef5bf9b src/HOL/Codegenerator_Test/Code_Test_Scala.thy --- a/src/HOL/Codegenerator_Test/Code_Test_Scala.thy Sun Dec 22 08:46:03 2024 +0100 +++ b/src/HOL/Codegenerator_Test/Code_Test_Scala.thy Mon Dec 23 21:22:10 2024 +0100 @@ -1,10 +1,14 @@ (* Title: HOL/Codegenerator_Test/Code_Test_Scala.thy Author: Andreas Lochbihler, ETH Zurich - -Test case for test_code on Scala + Author: Florian Haftmann, TU Muenchen *) -theory Code_Test_Scala imports "HOL-Library.Code_Test" Code_Lazy_Test begin +theory Code_Test_Scala imports + "HOL-Library.Code_Test" + Code_Lazy_Test +begin + +text \Test cases for \<^text>\test_code\\ test_code "14 + 7 * -12 = (140 div -2 :: integer)" in Scala @@ -22,4 +26,163 @@ 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