equal
deleted
inserted
replaced
96 else 0)" |
96 else 0)" |
97 |
97 |
98 definition Gcd_eucl :: "'a set \<Rightarrow> 'a" |
98 definition Gcd_eucl :: "'a set \<Rightarrow> 'a" |
99 where |
99 where |
100 "Gcd_eucl A = Lcm_eucl {d. \<forall>a\<in>A. d dvd a}" |
100 "Gcd_eucl A = Lcm_eucl {d. \<forall>a\<in>A. d dvd a}" |
|
101 |
|
102 declare Lcm_eucl_def Gcd_eucl_def [code del] |
101 |
103 |
102 lemma gcd_eucl_0: |
104 lemma gcd_eucl_0: |
103 "gcd_eucl a 0 = normalize a" |
105 "gcd_eucl a 0 = normalize a" |
104 by (simp add: gcd_eucl.simps [of a 0]) |
106 by (simp add: gcd_eucl.simps [of a 0]) |
105 |
107 |
957 assumes "finite A" |
959 assumes "finite A" |
958 shows "Lcm A = Finite_Set.fold lcm 1 A" |
960 shows "Lcm A = Finite_Set.fold lcm 1 A" |
959 by (induct rule: finite.induct[OF \<open>finite A\<close>]) |
961 by (induct rule: finite.induct[OF \<open>finite A\<close>]) |
960 (simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_lcm]) |
962 (simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_lcm]) |
961 |
963 |
962 lemma Lcm_set [code_unfold]: |
964 lemma Lcm_set: |
963 "Lcm (set xs) = fold lcm xs 1" |
965 "Lcm (set xs) = foldl lcm 1 xs" |
964 using comp_fun_idem.fold_set_fold[OF comp_fun_idem_lcm] Lcm_finite by (simp add: ac_simps) |
966 using comp_fun_idem.fold_set_fold[OF comp_fun_idem_lcm] Lcm_finite |
|
967 by (simp add: foldl_conv_fold lcm.commute) |
|
968 |
|
969 lemma Lcm_eucl_set [code]: |
|
970 "Lcm_eucl (set xs) = foldl lcm_eucl 1 xs" |
|
971 by (simp add: Lcm_Lcm_eucl [symmetric] lcm_lcm_eucl Lcm_set) |
965 |
972 |
966 lemma Lcm_singleton [simp]: |
973 lemma Lcm_singleton [simp]: |
967 "Lcm {a} = normalize a" |
974 "Lcm {a} = normalize a" |
968 by simp |
975 by simp |
969 |
976 |
1011 assumes "finite A" |
1018 assumes "finite A" |
1012 shows "Gcd A = Finite_Set.fold gcd 0 A" |
1019 shows "Gcd A = Finite_Set.fold gcd 0 A" |
1013 by (induct rule: finite.induct[OF \<open>finite A\<close>]) |
1020 by (induct rule: finite.induct[OF \<open>finite A\<close>]) |
1014 (simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_gcd]) |
1021 (simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_gcd]) |
1015 |
1022 |
1016 lemma Gcd_set [code_unfold]: |
1023 lemma Gcd_set: |
1017 "Gcd (set xs) = fold gcd xs 0" |
1024 "Gcd (set xs) = foldl gcd 0 xs" |
1018 using comp_fun_idem.fold_set_fold[OF comp_fun_idem_gcd] Gcd_finite by (simp add: ac_simps) |
1025 using comp_fun_idem.fold_set_fold[OF comp_fun_idem_gcd] Gcd_finite |
|
1026 by (simp add: foldl_conv_fold gcd.commute) |
|
1027 |
|
1028 lemma Gcd_eucl_set [code]: |
|
1029 "Gcd_eucl (set xs) = foldl gcd_eucl 0 xs" |
|
1030 by (simp add: Gcd_Gcd_eucl [symmetric] gcd_gcd_eucl Gcd_set) |
1019 |
1031 |
1020 lemma Gcd_singleton [simp]: "Gcd {a} = normalize a" |
1032 lemma Gcd_singleton [simp]: "Gcd {a} = normalize a" |
1021 by simp |
1033 by simp |
1022 |
1034 |
1023 lemma Gcd_2 [simp]: "Gcd {a,b} = gcd a b" |
1035 lemma Gcd_2 [simp]: "Gcd {a,b} = gcd a b" |