# HG changeset patch # User Andreas Lochbihler # Date 1450433668 -3600 # Node ID 4b1b85f3894403abc93a1a27b932a487a10b46df # Parent 32a530a5c54cfa3bd5263600e3bdfae87153627e add gcd instance for integer and serialisation to target language operations diff -r 32a530a5c54c -r 4b1b85f38944 src/HOL/Codegenerator_Test/Code_Test_GHC.thy --- a/src/HOL/Codegenerator_Test/Code_Test_GHC.thy Wed Dec 16 17:30:30 2015 +0100 +++ b/src/HOL/Codegenerator_Test/Code_Test_GHC.thy Fri Dec 18 11:14:28 2015 +0100 @@ -4,10 +4,20 @@ Test case for test_code on GHC *) -theory Code_Test_GHC imports "../Library/Code_Test" begin +theory Code_Test_GHC imports "../Library/Code_Test" "../GCD" begin test_code "(14 + 7 * -12 :: integer) = 140 div -2" in GHC value [GHC] "14 + 7 * -12 :: integer" +test_code -- \Tests for the serialisation of @{const gcd} on @{typ integer}\ + "gcd 15 10 = (5 :: integer)" + "gcd 15 (- 10) = (5 :: integer)" + "gcd (- 10) 15 = (5 :: integer)" + "gcd (- 10) (- 15) = (5 :: integer)" + "gcd 0 (- 10) = (10 :: integer)" + "gcd (- 10) 0 = (10 :: integer)" + "gcd 0 0 = (0 :: integer)" +in GHC + end diff -r 32a530a5c54c -r 4b1b85f38944 src/HOL/Codegenerator_Test/Code_Test_OCaml.thy --- a/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy Wed Dec 16 17:30:30 2015 +0100 +++ b/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy Fri Dec 18 11:14:28 2015 +0100 @@ -4,10 +4,20 @@ Test case for test_code on OCaml *) -theory Code_Test_OCaml imports "../Library/Code_Test" begin +theory Code_Test_OCaml imports "../Library/Code_Test" "../GCD" begin test_code "14 + 7 * -12 = (140 div -2 :: integer)" in OCaml value [OCaml] "14 + 7 * -12 :: integer" +test_code -- \Tests for the serialisation of @{const gcd} on @{typ integer}\ + "gcd 15 10 = (5 :: integer)" + "gcd 15 (- 10) = (5 :: integer)" + "gcd (- 10) 15 = (5 :: integer)" + "gcd (- 10) (- 15) = (5 :: integer)" + "gcd 0 (- 10) = (10 :: integer)" + "gcd (- 10) 0 = (10 :: integer)" + "gcd 0 0 = (0 :: integer)" +in OCaml + end diff -r 32a530a5c54c -r 4b1b85f38944 src/HOL/Codegenerator_Test/Code_Test_Scala.thy --- a/src/HOL/Codegenerator_Test/Code_Test_Scala.thy Wed Dec 16 17:30:30 2015 +0100 +++ b/src/HOL/Codegenerator_Test/Code_Test_Scala.thy Fri Dec 18 11:14:28 2015 +0100 @@ -4,7 +4,7 @@ Test case for test_code on Scala *) -theory Code_Test_Scala imports "../Library/Code_Test" begin +theory Code_Test_Scala imports "../Library/Code_Test" "../GCD" begin declare [[scala_case_insensitive]] @@ -12,4 +12,14 @@ value [Scala] "14 + 7 * -12 :: integer" +test_code -- \Tests for the serialisation of @{const gcd} on @{typ integer}\ + "gcd 15 10 = (5 :: integer)" + "gcd 15 (- 10) = (5 :: integer)" + "gcd (- 10) 15 = (5 :: integer)" + "gcd (- 10) (- 15) = (5 :: integer)" + "gcd 0 (- 10) = (10 :: integer)" + "gcd (- 10) 0 = (10 :: integer)" + "gcd 0 0 = (0 :: integer)" +in Scala + end diff -r 32a530a5c54c -r 4b1b85f38944 src/HOL/GCD.thy --- a/src/HOL/GCD.thy Wed Dec 16 17:30:30 2015 +0100 +++ b/src/HOL/GCD.thy Fri Dec 18 11:14:28 2015 +0100 @@ -2196,4 +2196,33 @@ lemmas Gcd_empty_int = Gcd_empty [where ?'a = int] and Gcd_insert_int = Gcd_insert [where ?'a = int] +subsection \gcd and lcm instances for @{typ integer}\ + +instantiation integer :: gcd begin +context includes integer.lifting begin +lift_definition gcd_integer :: "integer \ integer \ integer" is gcd . +lift_definition lcm_integer :: "integer \ integer \ integer" is lcm . end +instance .. +end +lifting_update integer.lifting +lifting_forget integer.lifting + +context includes integer.lifting begin + +lemma gcd_code_integer [code]: + "gcd k l = \if l = (0::integer) then k else gcd l (\k\ mod \l\)\" +by transfer(fact gcd_code_int) + +lemma lcm_code_integer [code]: "lcm (a::integer) b = (abs a) * (abs b) div gcd a b" +by transfer(fact lcm_altdef_int) + +end + +code_printing constant "gcd :: integer \ _" + \ (OCaml) "Big'_int.gcd'_big'_int" + and (Haskell) "Prelude.gcd" + and (Scala) "_.gcd'((_)')" + -- \There is no gcd operation in the SML standard library, so no code setup for SML\ + +end diff -r 32a530a5c54c -r 4b1b85f38944 src/HOL/Library/Code_Target_Int.thy --- a/src/HOL/Library/Code_Target_Int.thy Wed Dec 16 17:30:30 2015 +0100 +++ b/src/HOL/Library/Code_Target_Int.thy Fri Dec 18 11:14:28 2015 +0100 @@ -5,7 +5,7 @@ section \Implementation of integer numbers by target-language integers\ theory Code_Target_Int -imports Main +imports "../GCD" begin code_datatype int_of_integer @@ -94,6 +94,15 @@ lemma [code]: "k < l \ (of_int k :: integer) < of_int l" by transfer rule + +lemma gcd_int_of_integer [code]: + "gcd (int_of_integer x) (int_of_integer y) = int_of_integer (gcd x y)" +by transfer rule + +lemma lcm_int_of_integer [code]: + "lcm (int_of_integer x) (int_of_integer y) = int_of_integer (lcm x y)" +by transfer rule + end lemma (in ring_1) of_int_code_if: