proper code equations for Gcd and Lcm on nat and int
authorhaftmann
Fri Nov 15 22:02:01 2013 +0100 (2013-11-15)
changeset 544370060957404c7
parent 54436 0e1c576bbc19
child 54438 82ef58dba83b
proper code equations for Gcd and Lcm on nat and int
src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
src/HOL/GCD.thy
     1.1 --- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Sat Nov 16 07:45:53 2013 +0100
     1.2 +++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Fri Nov 15 22:02:01 2013 +0100
     1.3 @@ -40,6 +40,18 @@
     1.4  lemma [code, code del]:
     1.5    "Cardinality.eq_set = Cardinality.eq_set" ..
     1.6  
     1.7 +lemma [code, code del]:
     1.8 +  "(Gcd :: nat set \<Rightarrow> nat) = Gcd" ..
     1.9 +
    1.10 +lemma [code, code del]:
    1.11 +  "(Lcm :: nat set \<Rightarrow> nat) = Lcm" ..
    1.12 +
    1.13 +lemma [code, code del]:
    1.14 +  "(Gcd :: int set \<Rightarrow> int) = Gcd" ..
    1.15 +
    1.16 +lemma [code, code del]:
    1.17 +  "(Lcm :: int set \<Rightarrow> int) = Lcm" ..
    1.18 +  
    1.19  (*
    1.20    If the code generation ends with an exception with the following message:
    1.21    '"List.set" is not a constructor, on left hand side of equation: ...',
     2.1 --- a/src/HOL/GCD.thy	Sat Nov 16 07:45:53 2013 +0100
     2.2 +++ b/src/HOL/GCD.thy	Fri Nov 15 22:02:01 2013 +0100
     2.3 @@ -1654,11 +1654,11 @@
     2.4  apply (metis Lcm0_iff dvd_Lcm_nat dvd_imp_le neq0_conv)
     2.5  done
     2.6  
     2.7 -lemma Lcm_set_nat [code_unfold]:
     2.8 +lemma Lcm_set_nat [code, code_unfold]:
     2.9    "Lcm (set ns) = fold lcm ns (1::nat)"
    2.10    by (fact gcd_lcm_complete_lattice_nat.Sup_set_fold)
    2.11  
    2.12 -lemma Gcd_set_nat [code_unfold]:
    2.13 +lemma Gcd_set_nat [code, code_unfold]:
    2.14    "Gcd (set ns) = fold gcd ns (0::nat)"
    2.15    by (fact gcd_lcm_complete_lattice_nat.Inf_set_fold)
    2.16  
    2.17 @@ -1730,11 +1730,11 @@
    2.18    assumes "\<forall>m\<in>M. n dvd m" shows "n dvd Gcd M"
    2.19    using assms by (simp add: Gcd_int_def dvd_int_iff)
    2.20  
    2.21 -lemma Lcm_set_int [code_unfold]:
    2.22 +lemma Lcm_set_int [code, code_unfold]:
    2.23    "Lcm (set xs) = fold lcm xs (1::int)"
    2.24    by (induct xs rule: rev_induct, simp_all add: lcm_commute_int)
    2.25  
    2.26 -lemma Gcd_set_int [code_unfold]:
    2.27 +lemma Gcd_set_int [code, code_unfold]:
    2.28    "Gcd (set xs) = fold gcd xs (0::int)"
    2.29    by (induct xs rule: rev_induct, simp_all add: gcd_commute_int)
    2.30