# HG changeset patch
# User haftmann
# Date 1384549321 -3600
# Node ID 0060957404c701e585daeb65e64762a6c25be5ff
# Parent  0e1c576bbc190d2d7ac5e07a8d25c3a08748080b
proper code equations for Gcd and Lcm on nat and int

diff -r 0e1c576bbc19 -r 0060957404c7 src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
--- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Sat Nov 16 07:45:53 2013 +0100
+++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Fri Nov 15 22:02:01 2013 +0100
@@ -40,6 +40,18 @@
 lemma [code, code del]:
   "Cardinality.eq_set = Cardinality.eq_set" ..
 
+lemma [code, code del]:
+  "(Gcd :: nat set \<Rightarrow> nat) = Gcd" ..
+
+lemma [code, code del]:
+  "(Lcm :: nat set \<Rightarrow> nat) = Lcm" ..
+
+lemma [code, code del]:
+  "(Gcd :: int set \<Rightarrow> int) = Gcd" ..
+
+lemma [code, code del]:
+  "(Lcm :: int set \<Rightarrow> int) = Lcm" ..
+  
 (*
   If the code generation ends with an exception with the following message:
   '"List.set" is not a constructor, on left hand side of equation: ...',
diff -r 0e1c576bbc19 -r 0060957404c7 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Sat Nov 16 07:45:53 2013 +0100
+++ b/src/HOL/GCD.thy	Fri Nov 15 22:02:01 2013 +0100
@@ -1654,11 +1654,11 @@
 apply (metis Lcm0_iff dvd_Lcm_nat dvd_imp_le neq0_conv)
 done
 
-lemma Lcm_set_nat [code_unfold]:
+lemma Lcm_set_nat [code, code_unfold]:
   "Lcm (set ns) = fold lcm ns (1::nat)"
   by (fact gcd_lcm_complete_lattice_nat.Sup_set_fold)
 
-lemma Gcd_set_nat [code_unfold]:
+lemma Gcd_set_nat [code, code_unfold]:
   "Gcd (set ns) = fold gcd ns (0::nat)"
   by (fact gcd_lcm_complete_lattice_nat.Inf_set_fold)
 
@@ -1730,11 +1730,11 @@
   assumes "\<forall>m\<in>M. n dvd m" shows "n dvd Gcd M"
   using assms by (simp add: Gcd_int_def dvd_int_iff)
 
-lemma Lcm_set_int [code_unfold]:
+lemma Lcm_set_int [code, code_unfold]:
   "Lcm (set xs) = fold lcm xs (1::int)"
   by (induct xs rule: rev_induct, simp_all add: lcm_commute_int)
 
-lemma Gcd_set_int [code_unfold]:
+lemma Gcd_set_int [code, code_unfold]:
   "Gcd (set xs) = fold gcd xs (0::int)"
   by (induct xs rule: rev_induct, simp_all add: gcd_commute_int)