--- 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: ...',
--- 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)