Fixed code equations for Gcd/Lcm
authorManuel Eberl <eberlm@in.tum.de>
Fri Feb 26 18:33:01 2016 +0100 (2016-02-26)
changeset 624284d5fbec92bb1
parent 62427 6dce7bf7960b
child 62429 25271ff79171
Fixed code equations for Gcd/Lcm
src/HOL/Number_Theory/Euclidean_Algorithm.thy
     1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Fri Feb 26 15:49:35 2016 +0100
     1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Fri Feb 26 18:33:01 2016 +0100
     1.3 @@ -99,6 +99,8 @@
     1.4  where
     1.5    "Gcd_eucl A = Lcm_eucl {d. \<forall>a\<in>A. d dvd a}"
     1.6  
     1.7 +declare Lcm_eucl_def Gcd_eucl_def [code del]
     1.8 +
     1.9  lemma gcd_eucl_0:
    1.10    "gcd_eucl a 0 = normalize a"
    1.11    by (simp add: gcd_eucl.simps [of a 0])
    1.12 @@ -959,9 +961,14 @@
    1.13    by (induct rule: finite.induct[OF \<open>finite A\<close>])
    1.14      (simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_lcm])
    1.15  
    1.16 -lemma Lcm_set [code_unfold]:
    1.17 -  "Lcm (set xs) = fold lcm xs 1"
    1.18 -  using comp_fun_idem.fold_set_fold[OF comp_fun_idem_lcm] Lcm_finite by (simp add: ac_simps)
    1.19 +lemma Lcm_set:
    1.20 +  "Lcm (set xs) = foldl lcm 1 xs"
    1.21 +  using comp_fun_idem.fold_set_fold[OF comp_fun_idem_lcm] Lcm_finite
    1.22 +  by (simp add: foldl_conv_fold lcm.commute)
    1.23 +
    1.24 +lemma Lcm_eucl_set [code]:
    1.25 +  "Lcm_eucl (set xs) = foldl lcm_eucl 1 xs"
    1.26 +  by (simp add: Lcm_Lcm_eucl [symmetric] lcm_lcm_eucl Lcm_set)
    1.27  
    1.28  lemma Lcm_singleton [simp]:
    1.29    "Lcm {a} = normalize a"
    1.30 @@ -1013,9 +1020,14 @@
    1.31    by (induct rule: finite.induct[OF \<open>finite A\<close>])
    1.32      (simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_gcd])
    1.33  
    1.34 -lemma Gcd_set [code_unfold]:
    1.35 -  "Gcd (set xs) = fold gcd xs 0"
    1.36 -  using comp_fun_idem.fold_set_fold[OF comp_fun_idem_gcd] Gcd_finite by (simp add: ac_simps)
    1.37 +lemma Gcd_set:
    1.38 +  "Gcd (set xs) = foldl gcd 0 xs"
    1.39 +  using comp_fun_idem.fold_set_fold[OF comp_fun_idem_gcd] Gcd_finite
    1.40 +  by (simp add: foldl_conv_fold gcd.commute)
    1.41 +
    1.42 +lemma Gcd_eucl_set [code]:
    1.43 +  "Gcd_eucl (set xs) = foldl gcd_eucl 0 xs"
    1.44 +  by (simp add: Gcd_Gcd_eucl [symmetric] gcd_gcd_eucl Gcd_set)
    1.45  
    1.46  lemma Gcd_singleton [simp]: "Gcd {a} = normalize a"
    1.47    by simp