# 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 -- \<open>Tests for the serialisation of @{const gcd} on @{typ integer}\<close>
+  "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 -- \<open>Tests for the serialisation of @{const gcd} on @{typ integer}\<close>
+  "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 -- \<open>Tests for the serialisation of @{const gcd} on @{typ integer}\<close>
+  "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 \<open>gcd and lcm instances for @{typ integer}\<close>
+
+instantiation integer :: gcd begin
+context includes integer.lifting begin
+lift_definition gcd_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer" is gcd .
+lift_definition lcm_integer :: "integer \<Rightarrow> integer \<Rightarrow> 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 = \<bar>if l = (0::integer) then k else gcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
+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 \<Rightarrow> _"
+  \<rightharpoonup> (OCaml) "Big'_int.gcd'_big'_int"
+  and (Haskell) "Prelude.gcd"
+  and (Scala) "_.gcd'((_)')"
+  -- \<open>There is no gcd operation in the SML standard library, so no code setup for SML\<close>
+
+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 \<open>Implementation of integer numbers by target-language integers\<close>
 
 theory Code_Target_Int
-imports Main
+imports "../GCD"
 begin
 
 code_datatype int_of_integer
@@ -94,6 +94,15 @@
 lemma [code]:
   "k < l \<longleftrightarrow> (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: