--- a/src/HOL/Code_Numeral.thy Mon Jan 09 19:34:02 2017 +0100
+++ b/src/HOL/Code_Numeral.thy Mon Jan 09 19:34:16 2017 +0100
@@ -225,7 +225,7 @@
"of_nat (nat_of_integer k) = max 0 k"
by transfer auto
-instantiation integer :: "{ring_div, normalization_semidom}"
+instantiation integer :: normalization_semidom
begin
lift_definition normalize_integer :: "integer \<Rightarrow> integer"
@@ -245,7 +245,16 @@
.
declare divide_integer.rep_eq [simp]
+
+instance
+ by (standard; transfer)
+ (auto simp add: mult_sgn_abs sgn_mult abs_eq_iff')
+end
+
+instantiation integer :: ring_div
+begin
+
lift_definition modulo_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
is "modulo :: int \<Rightarrow> int \<Rightarrow> int"
.
@@ -253,7 +262,7 @@
declare modulo_integer.rep_eq [simp]
instance
- by standard (transfer, simp add: mult_sgn_abs sgn_mult)+
+ by (standard; transfer) simp_all
end
--- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy Mon Jan 09 19:34:02 2017 +0100
+++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy Mon Jan 09 19:34:16 2017 +0100
@@ -34,6 +34,8 @@
Cardinality.finite'
Cardinality.subset'
Cardinality.eq_set
+ Gcd_fin
+ Lcm_fin
"Gcd :: nat set \<Rightarrow> nat"
"Lcm :: nat set \<Rightarrow> nat"
"Gcd :: int set \<Rightarrow> int"
--- a/src/HOL/Divides.thy Mon Jan 09 19:34:02 2017 +0100
+++ b/src/HOL/Divides.thy Mon Jan 09 19:34:16 2017 +0100
@@ -1812,7 +1812,7 @@
assume "l \<noteq> 0"
then show "k * l div l = k"
by (auto simp add: eucl_rel_int_iff ac_simps intro: div_int_unique [of _ _ _ 0])
-qed (simp_all add: sgn_mult mult_sgn_abs abs_sgn_eq)
+qed (auto simp add: sgn_mult mult_sgn_abs abs_eq_iff')
end
--- a/src/HOL/GCD.thy Mon Jan 09 19:34:02 2017 +0100
+++ b/src/HOL/GCD.thy Mon Jan 09 19:34:16 2017 +0100
@@ -34,6 +34,108 @@
imports Main
begin
+subsection \<open>Abstract bounded quasi semilattices as common foundation\<close>
+
+locale bounded_quasi_semilattice = abel_semigroup +
+ fixes top :: 'a ("\<top>") and bot :: 'a ("\<bottom>")
+ and normalize :: "'a \<Rightarrow> 'a"
+ assumes idem_normalize [simp]: "a \<^bold>* a = normalize a"
+ and normalize_left_idem [simp]: "normalize a \<^bold>* b = a \<^bold>* b"
+ and normalize_idem [simp]: "normalize (a \<^bold>* b) = a \<^bold>* b"
+ and normalize_top [simp]: "normalize \<top> = \<top>"
+ and normalize_bottom [simp]: "normalize \<bottom> = \<bottom>"
+ and top_left_normalize [simp]: "\<top> \<^bold>* a = normalize a"
+ and bottom_left_bottom [simp]: "\<bottom> \<^bold>* a = \<bottom>"
+begin
+
+lemma left_idem [simp]:
+ "a \<^bold>* (a \<^bold>* b) = a \<^bold>* b"
+ using assoc [of a a b, symmetric] by simp
+
+lemma right_idem [simp]:
+ "(a \<^bold>* b) \<^bold>* b = a \<^bold>* b"
+ using left_idem [of b a] by (simp add: ac_simps)
+
+lemma comp_fun_idem: "comp_fun_idem f"
+ by standard (simp_all add: fun_eq_iff ac_simps)
+
+interpretation comp_fun_idem f
+ by (fact comp_fun_idem)
+
+lemma top_right_normalize [simp]:
+ "a \<^bold>* \<top> = normalize a"
+ using top_left_normalize [of a] by (simp add: ac_simps)
+
+lemma bottom_right_bottom [simp]:
+ "a \<^bold>* \<bottom> = \<bottom>"
+ using bottom_left_bottom [of a] by (simp add: ac_simps)
+
+lemma normalize_right_idem [simp]:
+ "a \<^bold>* normalize b = a \<^bold>* b"
+ using normalize_left_idem [of b a] by (simp add: ac_simps)
+
+end
+
+locale bounded_quasi_semilattice_set = bounded_quasi_semilattice
+begin
+
+interpretation comp_fun_idem f
+ by (fact comp_fun_idem)
+
+definition F :: "'a set \<Rightarrow> 'a"
+where
+ eq_fold: "F A = (if finite A then Finite_Set.fold f \<top> A else \<bottom>)"
+
+lemma set_eq_fold [code]:
+ "F (set xs) = fold f xs \<top>"
+ by (simp add: eq_fold fold_set_fold)
+
+lemma infinite [simp]:
+ "infinite A \<Longrightarrow> F A = \<bottom>"
+ by (simp add: eq_fold)
+
+lemma empty [simp]:
+ "F {} = \<top>"
+ by (simp add: eq_fold)
+
+lemma insert [simp]:
+ "F (insert a A) = a \<^bold>* F A"
+ by (cases "finite A") (simp_all add: eq_fold)
+
+lemma normalize [simp]:
+ "normalize (F A) = F A"
+ by (induct A rule: infinite_finite_induct) simp_all
+
+lemma in_idem:
+ assumes "a \<in> A"
+ shows "a \<^bold>* F A = F A"
+ using assms by (induct A rule: infinite_finite_induct)
+ (auto simp add: left_commute [of a])
+
+lemma union:
+ "F (A \<union> B) = F A \<^bold>* F B"
+ by (induct A rule: infinite_finite_induct)
+ (simp_all add: ac_simps)
+
+lemma remove:
+ assumes "a \<in> A"
+ shows "F A = a \<^bold>* F (A - {a})"
+proof -
+ from assms obtain B where "A = insert a B" and "a \<notin> B"
+ by (blast dest: mk_disjoint_insert)
+ with assms show ?thesis by simp
+qed
+
+lemma insert_remove:
+ "F (insert a A) = a \<^bold>* F (A - {a})"
+ by (cases "a \<in> A") (simp_all add: insert_absorb remove)
+
+lemma subset:
+ assumes "B \<subseteq> A"
+ shows "F B \<^bold>* F A = F A"
+ using assms by (simp add: union [symmetric] Un_absorb1)
+
+end
subsection \<open>Abstract GCD and LCM\<close>
@@ -165,25 +267,36 @@
by (rule associated_eqI) simp_all
qed
-lemma gcd_self [simp]: "gcd a a = normalize a"
-proof -
- have "a dvd gcd a a"
- by (rule gcd_greatest) simp_all
- then show ?thesis
+sublocale gcd: bounded_quasi_semilattice gcd 0 1 normalize
+proof
+ show "gcd a a = normalize a" for a
+ proof -
+ have "a dvd gcd a a"
+ by (rule gcd_greatest) simp_all
+ then show ?thesis
+ by (auto intro: associated_eqI)
+ qed
+ show "gcd (normalize a) b = gcd a b" for a b
+ using gcd_dvd1 [of "normalize a" b]
by (auto intro: associated_eqI)
-qed
-
-lemma gcd_left_idem [simp]: "gcd a (gcd a b) = gcd a b"
- by (auto intro: associated_eqI)
-
-lemma gcd_right_idem [simp]: "gcd (gcd a b) b = gcd a b"
- unfolding gcd.commute [of a] gcd.commute [of "gcd b a"] by simp
-
-lemma coprime_1_left [simp]: "coprime 1 a"
- by (rule associated_eqI) simp_all
-
-lemma coprime_1_right [simp]: "coprime a 1"
- using coprime_1_left [of a] by (simp add: ac_simps)
+ show "coprime 1 a" for a
+ by (rule associated_eqI) simp_all
+qed simp_all
+
+lemma gcd_self: "gcd a a = normalize a"
+ by (fact gcd.idem_normalize)
+
+lemma gcd_left_idem: "gcd a (gcd a b) = gcd a b"
+ by (fact gcd.left_idem)
+
+lemma gcd_right_idem: "gcd (gcd a b) b = gcd a b"
+ by (fact gcd.right_idem)
+
+lemma coprime_1_left: "coprime 1 a"
+ by (fact gcd.bottom_left_bottom)
+
+lemma coprime_1_right: "coprime a 1"
+ by (fact gcd.bottom_right_bottom)
lemma gcd_mult_left: "gcd (c * a) (c * b) = normalize c * gcd a b"
proof (cases "c = 0")
@@ -325,19 +438,30 @@
by (rule associated_eqI) simp_all
qed
-lemma lcm_self [simp]: "lcm a a = normalize a"
-proof -
- have "lcm a a dvd a"
- by (rule lcm_least) simp_all
- then show ?thesis
+sublocale lcm: bounded_quasi_semilattice lcm 1 0 normalize
+proof
+ show "lcm a a = normalize a" for a
+ proof -
+ have "lcm a a dvd a"
+ by (rule lcm_least) simp_all
+ then show ?thesis
+ by (auto intro: associated_eqI)
+ qed
+ show "lcm (normalize a) b = lcm a b" for a b
+ using dvd_lcm1 [of "normalize a" b] unfolding normalize_dvd_iff
by (auto intro: associated_eqI)
-qed
-
-lemma lcm_left_idem [simp]: "lcm a (lcm a b) = lcm a b"
- by (auto intro: associated_eqI)
-
-lemma lcm_right_idem [simp]: "lcm (lcm a b) b = lcm a b"
- unfolding lcm.commute [of a] lcm.commute [of "lcm b a"] by simp
+ show "lcm 1 a = normalize a" for a
+ by (rule associated_eqI) simp_all
+qed simp_all
+
+lemma lcm_self: "lcm a a = normalize a"
+ by (fact lcm.idem_normalize)
+
+lemma lcm_left_idem: "lcm a (lcm a b) = lcm a b"
+ by (fact lcm.left_idem)
+
+lemma lcm_right_idem: "lcm (lcm a b) b = lcm a b"
+ by (fact lcm.right_idem)
lemma gcd_mult_lcm [simp]: "gcd a b * lcm a b = normalize a * normalize b"
by (simp add: lcm_gcd normalize_mult)
@@ -359,11 +483,11 @@
using nonzero_mult_div_cancel_right [of "lcm a b" "gcd a b"] by simp
qed
-lemma lcm_1_left [simp]: "lcm 1 a = normalize a"
- by (simp add: lcm_gcd)
-
-lemma lcm_1_right [simp]: "lcm a 1 = normalize a"
- by (simp add: lcm_gcd)
+lemma lcm_1_left: "lcm 1 a = normalize a"
+ by (fact lcm.top_left_normalize)
+
+lemma lcm_1_right: "lcm a 1 = normalize a"
+ by (fact lcm.top_right_normalize)
lemma lcm_mult_left: "lcm (c * a) (c * b) = normalize c * lcm a b"
by (cases "c = 0")
@@ -450,23 +574,11 @@
lemma lcm_div_unit2: "is_unit a \<Longrightarrow> lcm b (c div a) = lcm b c"
by (erule is_unitE [of _ c]) (simp add: lcm_mult_unit2)
-lemma normalize_lcm_left [simp]: "lcm (normalize a) b = lcm a b"
-proof (cases "a = 0")
- case True
- then show ?thesis
- by simp
-next
- case False
- then have "is_unit (unit_factor a)"
- by simp
- moreover have "normalize a = a div unit_factor a"
- by simp
- ultimately show ?thesis
- by (simp only: lcm_div_unit1)
-qed
-
-lemma normalize_lcm_right [simp]: "lcm a (normalize b) = lcm a b"
- using normalize_lcm_left [of b a] by (simp add: ac_simps)
+lemma normalize_lcm_left: "lcm (normalize a) b = lcm a b"
+ by (fact lcm.normalize_left_idem)
+
+lemma normalize_lcm_right: "lcm a (normalize b) = lcm a b"
+ by (fact lcm.normalize_right_idem)
lemma gcd_mult_unit1: "is_unit a \<Longrightarrow> gcd (b * a) c = gcd b c"
apply (rule gcdI)
@@ -489,23 +601,11 @@
lemma gcd_div_unit2: "is_unit a \<Longrightarrow> gcd b (c div a) = gcd b c"
by (erule is_unitE [of _ c]) (simp add: gcd_mult_unit2)
-lemma normalize_gcd_left [simp]: "gcd (normalize a) b = gcd a b"
-proof (cases "a = 0")
- case True
- then show ?thesis
- by simp
-next
- case False
- then have "is_unit (unit_factor a)"
- by simp
- moreover have "normalize a = a div unit_factor a"
- by simp
- ultimately show ?thesis
- by (simp only: gcd_div_unit1)
-qed
-
-lemma normalize_gcd_right [simp]: "gcd a (normalize b) = gcd a b"
- using normalize_gcd_left [of b a] by (simp add: ac_simps)
+lemma normalize_gcd_left: "gcd (normalize a) b = gcd a b"
+ by (fact gcd.normalize_left_idem)
+
+lemma normalize_gcd_right: "gcd a (normalize b) = gcd a b"
+ by (fact gcd.normalize_right_idem)
lemma comp_fun_idem_gcd: "comp_fun_idem gcd"
by standard (simp_all add: fun_eq_iff ac_simps)
@@ -942,6 +1042,21 @@
lemma lcm_proj2_iff: "lcm m n = normalize n \<longleftrightarrow> m dvd n"
using lcm_proj1_iff [of n m] by (simp add: ac_simps)
+lemma lcm_mult_distrib': "normalize c * lcm a b = lcm (c * a) (c * b)"
+ by (rule lcmI) (auto simp: normalize_mult lcm_least mult_dvd_mono lcm_mult_left [symmetric])
+
+lemma lcm_mult_distrib: "k * lcm a b = lcm (k * a) (k * b) * unit_factor k"
+proof-
+ have "normalize k * lcm a b = lcm (k * a) (k * b)"
+ by (simp add: lcm_mult_distrib')
+ then have "normalize k * lcm a b * unit_factor k = lcm (k * a) (k * b) * unit_factor k"
+ by simp
+ then have "normalize k * unit_factor k * lcm a b = lcm (k * a) (k * b) * unit_factor k"
+ by (simp only: ac_simps)
+ then show ?thesis
+ by simp
+qed
+
lemma dvd_productE:
assumes "p dvd (a * b)"
obtains x y where "p = x * y" "x dvd a" "y dvd b"
@@ -1229,26 +1344,6 @@
by (induct A rule: finite_ne_induct) (auto simp add: lcm_eq_0_iff)
qed
-lemma Gcd_finite:
- assumes "finite A"
- shows "Gcd A = Finite_Set.fold gcd 0 A"
- by (induct rule: finite.induct[OF \<open>finite A\<close>])
- (simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_gcd])
-
-lemma Gcd_set [code_unfold]: "Gcd (set as) = foldl gcd 0 as"
- by (simp add: Gcd_finite comp_fun_idem.fold_set_fold[OF comp_fun_idem_gcd]
- foldl_conv_fold gcd.commute)
-
-lemma Lcm_finite:
- assumes "finite A"
- shows "Lcm A = Finite_Set.fold lcm 1 A"
- by (induct rule: finite.induct[OF \<open>finite A\<close>])
- (simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_lcm])
-
-lemma Lcm_set [code_unfold]: "Lcm (set as) = foldl lcm 1 as"
- by (simp add: Lcm_finite comp_fun_idem.fold_set_fold[OF comp_fun_idem_lcm]
- foldl_conv_fold lcm.commute)
-
lemma Gcd_image_normalize [simp]: "Gcd (normalize ` A) = Gcd A"
proof -
have "Gcd (normalize ` A) dvd a" if "a \<in> A" for a
@@ -1432,6 +1527,145 @@
end
+
+subsection \<open>An aside: GCD and LCM on finite sets for incomplete gcd rings\<close>
+
+context semiring_gcd
+begin
+
+sublocale Gcd_fin: bounded_quasi_semilattice_set gcd 0 1 normalize
+defines
+ Gcd_fin ("Gcd\<^sub>f\<^sub>i\<^sub>n _" [900] 900) = "Gcd_fin.F :: 'a set \<Rightarrow> 'a" ..
+
+abbreviation gcd_list :: "'a list \<Rightarrow> 'a"
+ where "gcd_list xs \<equiv> Gcd\<^sub>f\<^sub>i\<^sub>n (set xs)"
+
+sublocale Lcm_fin: bounded_quasi_semilattice_set lcm 1 0 normalize
+defines
+ Lcm_fin ("Lcm\<^sub>f\<^sub>i\<^sub>n _" [900] 900) = Lcm_fin.F ..
+
+abbreviation lcm_list :: "'a list \<Rightarrow> 'a"
+ where "lcm_list xs \<equiv> Lcm\<^sub>f\<^sub>i\<^sub>n (set xs)"
+
+lemma Gcd_fin_dvd:
+ "a \<in> A \<Longrightarrow> Gcd\<^sub>f\<^sub>i\<^sub>n A dvd a"
+ by (induct A rule: infinite_finite_induct)
+ (auto intro: dvd_trans)
+
+lemma dvd_Lcm_fin:
+ "a \<in> A \<Longrightarrow> a dvd Lcm\<^sub>f\<^sub>i\<^sub>n A"
+ by (induct A rule: infinite_finite_induct)
+ (auto intro: dvd_trans)
+
+lemma Gcd_fin_greatest:
+ "a dvd Gcd\<^sub>f\<^sub>i\<^sub>n A" if "finite A" and "\<And>b. b \<in> A \<Longrightarrow> a dvd b"
+ using that by (induct A) simp_all
+
+lemma Lcm_fin_least:
+ "Lcm\<^sub>f\<^sub>i\<^sub>n A dvd a" if "finite A" and "\<And>b. b \<in> A \<Longrightarrow> b dvd a"
+ using that by (induct A) simp_all
+
+lemma gcd_list_greatest:
+ "a dvd gcd_list bs" if "\<And>b. b \<in> set bs \<Longrightarrow> a dvd b"
+ by (rule Gcd_fin_greatest) (simp_all add: that)
+
+lemma lcm_list_least:
+ "lcm_list bs dvd a" if "\<And>b. b \<in> set bs \<Longrightarrow> b dvd a"
+ by (rule Lcm_fin_least) (simp_all add: that)
+
+lemma dvd_Gcd_fin_iff:
+ "b dvd Gcd\<^sub>f\<^sub>i\<^sub>n A \<longleftrightarrow> (\<forall>a\<in>A. b dvd a)" if "finite A"
+ using that by (auto intro: Gcd_fin_greatest Gcd_fin_dvd dvd_trans [of b "Gcd\<^sub>f\<^sub>i\<^sub>n A"])
+
+lemma dvd_gcd_list_iff:
+ "b dvd gcd_list xs \<longleftrightarrow> (\<forall>a\<in>set xs. b dvd a)"
+ by (simp add: dvd_Gcd_fin_iff)
+
+lemma Lcm_fin_dvd_iff:
+ "Lcm\<^sub>f\<^sub>i\<^sub>n A dvd b \<longleftrightarrow> (\<forall>a\<in>A. a dvd b)" if "finite A"
+ using that by (auto intro: Lcm_fin_least dvd_Lcm_fin dvd_trans [of _ "Lcm\<^sub>f\<^sub>i\<^sub>n A" b])
+
+lemma lcm_list_dvd_iff:
+ "lcm_list xs dvd b \<longleftrightarrow> (\<forall>a\<in>set xs. a dvd b)"
+ by (simp add: Lcm_fin_dvd_iff)
+
+lemma Gcd_fin_mult:
+ "Gcd\<^sub>f\<^sub>i\<^sub>n (image (times b) A) = normalize b * Gcd\<^sub>f\<^sub>i\<^sub>n A" if "finite A"
+using that proof induct
+ case empty
+ then show ?case
+ by simp
+next
+ case (insert a A)
+ have "gcd (b * a) (b * Gcd\<^sub>f\<^sub>i\<^sub>n A) = gcd (b * a) (normalize (b * Gcd\<^sub>f\<^sub>i\<^sub>n A))"
+ by simp
+ also have "\<dots> = gcd (b * a) (normalize b * Gcd\<^sub>f\<^sub>i\<^sub>n A)"
+ by (simp add: normalize_mult)
+ finally show ?case
+ using insert by (simp add: gcd_mult_distrib')
+qed
+
+lemma Lcm_fin_mult:
+ "Lcm\<^sub>f\<^sub>i\<^sub>n (image (times b) A) = normalize b * Lcm\<^sub>f\<^sub>i\<^sub>n A" if "A \<noteq> {}"
+proof (cases "b = 0")
+ case True
+ moreover from that have "times 0 ` A = {0}"
+ by auto
+ ultimately show ?thesis
+ by simp
+next
+ case False
+ then have "inj (times b)"
+ by (rule inj_times)
+ show ?thesis proof (cases "finite A")
+ case False
+ moreover from \<open>inj (times b)\<close>
+ have "inj_on (times b) A"
+ by (rule inj_on_subset) simp
+ ultimately have "infinite (times b ` A)"
+ by (simp add: finite_image_iff)
+ with False show ?thesis
+ by simp
+ next
+ case True
+ then show ?thesis using that proof (induct A rule: finite_ne_induct)
+ case (singleton a)
+ then show ?case
+ by (simp add: normalize_mult)
+ next
+ case (insert a A)
+ have "lcm (b * a) (b * Lcm\<^sub>f\<^sub>i\<^sub>n A) = lcm (b * a) (normalize (b * Lcm\<^sub>f\<^sub>i\<^sub>n A))"
+ by simp
+ also have "\<dots> = lcm (b * a) (normalize b * Lcm\<^sub>f\<^sub>i\<^sub>n A)"
+ by (simp add: normalize_mult)
+ finally show ?case
+ using insert by (simp add: lcm_mult_distrib')
+ qed
+ qed
+qed
+
+end
+
+context semiring_Gcd
+begin
+
+lemma Gcd_fin_eq_Gcd [simp]:
+ "Gcd\<^sub>f\<^sub>i\<^sub>n A = Gcd A" if "finite A" for A :: "'a set"
+ using that by induct simp_all
+
+lemma Gcd_set_eq_fold [code_unfold]:
+ "Gcd (set xs) = fold gcd xs 0"
+ by (simp add: Gcd_fin.set_eq_fold [symmetric])
+
+lemma Lcm_fin_eq_Lcm [simp]:
+ "Lcm\<^sub>f\<^sub>i\<^sub>n A = Lcm A" if "finite A" for A :: "'a set"
+ using that by induct simp_all
+
+lemma Lcm_set_eq_fold [code_unfold]:
+ "Lcm (set xs) = fold lcm xs 1"
+ by (simp add: Lcm_fin.set_eq_fold [symmetric])
+
+end
subsection \<open>GCD and LCM on @{typ nat} and @{typ int}\<close>
@@ -2514,11 +2748,10 @@
text \<open>Some code equations\<close>
-lemmas Lcm_set_nat [code, code_unfold] = Lcm_set[where ?'a = nat]
-lemmas Gcd_set_nat [code] = Gcd_set[where ?'a = nat]
-lemmas Lcm_set_int [code, code_unfold] = Lcm_set[where ?'a = int]
-lemmas Gcd_set_int [code] = Gcd_set[where ?'a = int]
-
+lemmas Gcd_nat_set_eq_fold [code] = Gcd_set_eq_fold [where ?'a = nat]
+lemmas Lcm_nat_set_eq_fold [code] = Lcm_set_eq_fold [where ?'a = nat]
+lemmas Gcd_int_set_eq_fold [code] = Gcd_set_eq_fold [where ?'a = int]
+lemmas Lcm_int_set_eq_fold [code] = Lcm_set_eq_fold [where ?'a = int]
text \<open>Fact aliases.\<close>
--- a/src/HOL/Int.thy Mon Jan 09 19:34:02 2017 +0100
+++ b/src/HOL/Int.thy Mon Jan 09 19:34:16 2017 +0100
@@ -357,7 +357,6 @@
then show ?thesis ..
qed
-
end
text \<open>Comparisons involving @{term of_int}.\<close>
@@ -848,6 +847,13 @@
by simp
qed (auto elim!: Nats_cases)
+lemma (in idom_divide) of_int_divide_in_Ints:
+ "of_int a div of_int b \<in> \<int>" if "b dvd a"
+proof -
+ from that obtain c where "a = b * c" ..
+ then show ?thesis
+ by (cases "of_int b = 0") simp_all
+qed
text \<open>The premise involving @{term Ints} prevents @{term "a = 1/2"}.\<close>
--- a/src/HOL/Library/Polynomial.thy Mon Jan 09 19:34:02 2017 +0100
+++ b/src/HOL/Library/Polynomial.thy Mon Jan 09 19:34:16 2017 +0100
@@ -12,21 +12,6 @@
"~~/src/HOL/Library/Infinite_Set"
begin
-subsection \<open>Misc\<close>
-
-lemma quotient_of_denom_pos': "snd (quotient_of x) > 0"
- using quotient_of_denom_pos [OF surjective_pairing] .
-
-lemma of_int_divide_in_Ints:
- "b dvd a \<Longrightarrow> of_int a div of_int b \<in> (\<int> :: 'a :: idom_divide set)"
-proof (cases "of_int b = (0 :: 'a)")
- case False
- assume "b dvd a"
- then obtain c where "a = b * c" ..
- with \<open>of_int b \<noteq> (0::'a)\<close> show ?thesis by simp
-qed auto
-
-
subsection \<open>Auxiliary: operations for lists (later) representing coefficients\<close>
definition cCons :: "'a::zero \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "##" 65)
@@ -3423,59 +3408,104 @@
by force
qed
-instantiation poly :: ("{normalization_semidom, idom_divide}") normalization_semidom
+instantiation poly :: ("{semidom_divide_unit_factor, idom_divide}") normalization_semidom
begin
definition unit_factor_poly :: "'a poly \<Rightarrow> 'a poly"
- where "unit_factor_poly p = monom (unit_factor (lead_coeff p)) 0"
+ where "unit_factor_poly p = [:unit_factor (lead_coeff p):]"
definition normalize_poly :: "'a poly \<Rightarrow> 'a poly"
- where "normalize_poly p = map_poly (\<lambda>x. x div unit_factor (lead_coeff p)) p"
+ where "normalize p = p div [:unit_factor (lead_coeff p):]"
instance proof
fix p :: "'a poly"
show "unit_factor p * normalize p = p"
- by (cases "p = 0")
- (simp_all add: unit_factor_poly_def normalize_poly_def monom_0
- smult_conv_map_poly map_poly_map_poly o_def)
+ proof (cases "p = 0")
+ case True
+ then show ?thesis
+ by (simp add: unit_factor_poly_def normalize_poly_def)
+ next
+ case False
+ then have "lead_coeff p \<noteq> 0"
+ by simp
+ then have *: "unit_factor (lead_coeff p) \<noteq> 0"
+ using unit_factor_is_unit [of "lead_coeff p"] by auto
+ then have "unit_factor (lead_coeff p) dvd 1"
+ by (auto intro: unit_factor_is_unit)
+ then have **: "unit_factor (lead_coeff p) dvd c" for c
+ by (rule dvd_trans) simp
+ have ***: "unit_factor (lead_coeff p) * (c div unit_factor (lead_coeff p)) = c" for c
+ proof -
+ from ** obtain b where "c = unit_factor (lead_coeff p) * b" ..
+ then show ?thesis
+ using False * by simp
+ qed
+ have "p div [:unit_factor (lead_coeff p):] =
+ map_poly (\<lambda>c. c div unit_factor (lead_coeff p)) p"
+ by (simp add: const_poly_dvd_iff div_const_poly_conv_map_poly **)
+ then show ?thesis
+ by (simp add: normalize_poly_def unit_factor_poly_def
+ smult_conv_map_poly map_poly_map_poly o_def ***)
+ qed
next
fix p :: "'a poly"
assume "is_unit p"
- then obtain c where p: "p = [:c:]" "is_unit c"
+ then obtain c where p: "p = [:c:]" "c dvd 1"
by (auto simp: is_unit_poly_iff)
- thus "normalize p = 1"
- by (simp add: normalize_poly_def map_poly_pCons is_unit_normalize one_poly_def)
+ then show "unit_factor p = p"
+ by (simp add: unit_factor_poly_def monom_0 is_unit_unit_factor)
next
fix p :: "'a poly" assume "p \<noteq> 0"
- thus "is_unit (unit_factor p)"
- by (simp add: unit_factor_poly_def monom_0 is_unit_poly_iff)
+ then show "is_unit (unit_factor p)"
+ by (simp add: unit_factor_poly_def monom_0 is_unit_poly_iff unit_factor_is_unit)
qed (simp_all add: normalize_poly_def unit_factor_poly_def monom_0 lead_coeff_mult unit_factor_mult)
end
-lemma normalize_poly_eq_div:
- "normalize p = p div [:unit_factor (lead_coeff p):]"
-proof (cases "p = 0")
- case False
- thus ?thesis
- by (subst div_const_poly_conv_map_poly)
- (auto simp: normalize_poly_def const_poly_dvd_iff)
-qed (auto simp: normalize_poly_def)
+lemma normalize_poly_eq_map_poly:
+ "normalize p = map_poly (\<lambda>x. x div unit_factor (lead_coeff p)) p"
+proof -
+ have "[:unit_factor (lead_coeff p):] dvd p"
+ by (metis unit_factor_poly_def unit_factor_self)
+ then show ?thesis
+ by (simp add: normalize_poly_def div_const_poly_conv_map_poly)
+qed
+
+lemma coeff_normalize [simp]:
+ "coeff (normalize p) n = coeff p n div unit_factor (lead_coeff p)"
+ by (simp add: normalize_poly_eq_map_poly coeff_map_poly)
+
+class field_unit_factor = field + unit_factor +
+ assumes unit_factor_field [simp]: "unit_factor = id"
+begin
+
+subclass semidom_divide_unit_factor
+proof
+ fix a
+ assume "a \<noteq> 0"
+ then have "1 = a * inverse a"
+ by simp
+ then have "a dvd 1" ..
+ then show "unit_factor a dvd 1"
+ by simp
+qed simp_all
+
+end
lemma unit_factor_pCons:
- "unit_factor (pCons a p) = (if p = 0 then monom (unit_factor a) 0 else unit_factor p)"
+ "unit_factor (pCons a p) = (if p = 0 then [:unit_factor a:] else unit_factor p)"
by (simp add: unit_factor_poly_def)
lemma normalize_monom [simp]:
"normalize (monom a n) = monom (normalize a) n"
- by (cases "a = 0") (simp_all add: map_poly_monom normalize_poly_def degree_monom_eq)
+ by (cases "a = 0") (simp_all add: map_poly_monom normalize_poly_eq_map_poly degree_monom_eq)
lemma unit_factor_monom [simp]:
- "unit_factor (monom a n) = monom (unit_factor a) 0"
+ "unit_factor (monom a n) = [:unit_factor a:]"
by (cases "a = 0") (simp_all add: unit_factor_poly_def degree_monom_eq)
lemma normalize_const_poly: "normalize [:c:] = [:normalize c:]"
- by (simp add: normalize_poly_def map_poly_pCons)
+ by (simp add: normalize_poly_eq_map_poly map_poly_pCons)
lemma normalize_smult: "normalize (smult c p) = smult (normalize c) (normalize p)"
proof -
--- a/src/HOL/Library/Polynomial_Factorial.thy Mon Jan 09 19:34:02 2017 +0100
+++ b/src/HOL/Library/Polynomial_Factorial.thy Mon Jan 09 19:34:16 2017 +0100
@@ -520,8 +520,8 @@
(simp_all add: unit_factor_field_poly_def normalize_field_poly_def)
next
fix p :: "'a poly" assume "is_unit p"
- thus "normalize_field_poly p = 1"
- by (elim is_unit_polyE) (auto simp: normalize_field_poly_def monom_0 one_poly_def field_simps)
+ then show "unit_factor_field_poly p = p"
+ by (elim is_unit_polyE) (auto simp: unit_factor_field_poly_def monom_0 one_poly_def field_simps)
next
fix p :: "'a poly" assume "p \<noteq> 0"
thus "is_unit (unit_factor_field_poly p)"
@@ -566,7 +566,7 @@
proof -
have A: "class.comm_semiring_1 op * 1 op + (0 :: 'a poly)" ..
have B: "class.normalization_semidom op div op + op - (0 :: 'a poly) op * 1
- normalize_field_poly unit_factor_field_poly" ..
+ unit_factor_field_poly normalize_field_poly" ..
from field_poly.in_prime_factors_imp_prime [of p x] assms
show ?thesis unfolding prime_elem_def dvd_field_poly
comm_semiring_1.prime_elem_def[OF A] normalization_semidom.prime_def[OF B] by blast
@@ -981,12 +981,9 @@
shows "lcm p q = normalize (p * q) div gcd p q"
by (fact lcm_gcd)
-declare Gcd_set
- [where ?'a = "'a :: factorial_ring_gcd poly", code]
-
-declare Lcm_set
- [where ?'a = "'a :: factorial_ring_gcd poly", code]
-
+lemmas Gcd_poly_set_eq_fold [code] = Gcd_set_eq_fold [where ?'a = "'a :: factorial_ring_gcd poly"]
+lemmas Lcm_poly_set_eq_fold [code] = Lcm_set_eq_fold [where ?'a = "'a :: factorial_ring_gcd poly"]
+
text \<open>Example:
@{lemma "Lcm {[:1, 2, 3:], [:2, 3, 4:]} = [:[:2:], [:7:], [:16:], [:17:], [:12 :: int:]:]" by eval}
\<close>
--- a/src/HOL/Nat.thy Mon Jan 09 19:34:02 2017 +0100
+++ b/src/HOL/Nat.thy Mon Jan 09 19:34:16 2017 +0100
@@ -170,6 +170,28 @@
text \<open>Injectiveness and distinctness lemmas\<close>
+lemma (in semidom_divide) inj_times:
+ "inj (times a)" if "a \<noteq> 0"
+proof (rule injI)
+ fix b c
+ assume "a * b = a * c"
+ then have "a * b div a = a * c div a"
+ by (simp only:)
+ with that show "b = c"
+ by simp
+qed
+
+lemma (in cancel_ab_semigroup_add) inj_plus:
+ "inj (plus a)"
+proof (rule injI)
+ fix b c
+ assume "a + b = a + c"
+ then have "a + b - a = a + c - a"
+ by (simp only:)
+ then show "b = c"
+ by simp
+qed
+
lemma inj_Suc[simp]: "inj_on Suc N"
by (simp add: inj_on_def)
--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy Mon Jan 09 19:34:02 2017 +0100
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Mon Jan 09 19:34:16 2017 +0100
@@ -71,7 +71,7 @@
lemma semiring_gcd:
"class.semiring_gcd one zero times gcd lcm
- divide plus minus normalize unit_factor"
+ divide plus minus unit_factor normalize"
proof
show "gcd a b dvd a"
and "gcd a b dvd b" for a b
@@ -97,12 +97,12 @@
qed
interpretation semiring_gcd one zero times gcd lcm
- divide plus minus normalize unit_factor
+ divide plus minus unit_factor normalize
by (fact semiring_gcd)
lemma semiring_Gcd:
"class.semiring_Gcd one zero times gcd lcm Gcd Lcm
- divide plus minus normalize unit_factor"
+ divide plus minus unit_factor normalize"
proof -
show ?thesis
proof
@@ -180,13 +180,13 @@
qed
interpretation semiring_Gcd one zero times gcd lcm Gcd Lcm
- divide plus minus normalize unit_factor
+ divide plus minus unit_factor normalize
by (fact semiring_Gcd)
subclass factorial_semiring
proof -
show "class.factorial_semiring divide plus minus zero times one
- normalize unit_factor"
+ unit_factor normalize"
proof (standard, rule factorial_semiring_altI_aux) -- \<open>FIXME rule\<close>
fix x assume "x \<noteq> 0"
thus "finite {p. p dvd x \<and> normalize p = p}"
@@ -254,12 +254,12 @@
qed
lemma Gcd_eucl_set [code]:
- "Gcd (set xs) = foldl gcd 0 xs"
- by (fact local.Gcd_set)
+ "Gcd (set xs) = fold gcd xs 0"
+ by (fact Gcd_set_eq_fold)
lemma Lcm_eucl_set [code]:
- "Lcm (set xs) = foldl lcm 1 xs"
- by (fact local.Lcm_set)
+ "Lcm (set xs) = fold lcm xs 1"
+ by (fact Lcm_set_eq_fold)
end
@@ -406,7 +406,7 @@
interpret semiring_Gcd 1 0 times
Euclidean_Algorithm.gcd Euclidean_Algorithm.lcm
Euclidean_Algorithm.Gcd Euclidean_Algorithm.Lcm
- divide plus minus normalize unit_factor
+ divide plus minus unit_factor normalize
rewrites "dvd.dvd op * = Rings.dvd"
by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
show [simp]: "Euclidean_Algorithm.gcd = (gcd :: 'a \<Rightarrow> _)"
@@ -558,7 +558,7 @@
interpret semiring_Gcd 1 0 times
"Euclidean_Algorithm.gcd" "Euclidean_Algorithm.lcm"
"Euclidean_Algorithm.Gcd" "Euclidean_Algorithm.Lcm"
- divide plus minus normalize unit_factor
+ divide plus minus unit_factor normalize
rewrites "dvd.dvd op * = Rings.dvd"
by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
show [simp]: "(Euclidean_Algorithm.gcd :: nat \<Rightarrow> _) = gcd"
@@ -590,7 +590,7 @@
interpret semiring_Gcd 1 0 times
"Euclidean_Algorithm.gcd" "Euclidean_Algorithm.lcm"
"Euclidean_Algorithm.Gcd" "Euclidean_Algorithm.Lcm"
- divide plus minus normalize unit_factor
+ divide plus minus unit_factor normalize
rewrites "dvd.dvd op * = Rings.dvd"
by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
show [simp]: "(Euclidean_Algorithm.gcd :: int \<Rightarrow> _) = gcd"
--- a/src/HOL/Rat.thy Mon Jan 09 19:34:02 2017 +0100
+++ b/src/HOL/Rat.thy Mon Jan 09 19:34:16 2017 +0100
@@ -401,6 +401,9 @@
lemma quotient_of_denom_pos: "quotient_of r = (p, q) \<Longrightarrow> q > 0"
by (cases r) (simp add: quotient_of_Fract normalize_denom_pos)
+lemma quotient_of_denom_pos': "snd (quotient_of r) > 0"
+ using quotient_of_denom_pos [of r] by (simp add: prod_eq_iff)
+
lemma quotient_of_coprime: "quotient_of r = (p, q) \<Longrightarrow> coprime p q"
by (cases r) (simp add: quotient_of_Fract normalize_coprime)
--- a/src/HOL/Rings.thy Mon Jan 09 19:34:02 2017 +0100
+++ b/src/HOL/Rings.thy Mon Jan 09 19:34:16 2017 +0100
@@ -1156,15 +1156,20 @@
end
-class normalization_semidom = algebraic_semidom +
+class unit_factor =
+ fixes unit_factor :: "'a \<Rightarrow> 'a"
+
+class semidom_divide_unit_factor = semidom_divide + unit_factor +
+ assumes unit_factor_0 [simp]: "unit_factor 0 = 0"
+ and is_unit_unit_factor: "a dvd 1 \<Longrightarrow> unit_factor a = a"
+ and unit_factor_is_unit: "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd 1"
+ and unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b"
+ -- \<open>This fine-grained hierarchy will later on allow lean normalization of polynomials\<close>
+
+class normalization_semidom = algebraic_semidom + semidom_divide_unit_factor +
fixes normalize :: "'a \<Rightarrow> 'a"
- and unit_factor :: "'a \<Rightarrow> 'a"
assumes unit_factor_mult_normalize [simp]: "unit_factor a * normalize a = a"
and normalize_0 [simp]: "normalize 0 = 0"
- and unit_factor_0 [simp]: "unit_factor 0 = 0"
- and is_unit_normalize: "is_unit a \<Longrightarrow> normalize a = 1"
- and unit_factor_is_unit [iff]: "a \<noteq> 0 \<Longrightarrow> is_unit (unit_factor a)"
- and unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b"
begin
text \<open>
@@ -1176,6 +1181,8 @@
think about equality of normalized values rather than associated elements.
\<close>
+declare unit_factor_is_unit [iff]
+
lemma unit_factor_dvd [simp]: "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd b"
by (rule unit_imp_dvd) simp
@@ -1207,13 +1214,45 @@
then show ?lhs by simp
qed
-lemma is_unit_unit_factor:
+lemma div_unit_factor [simp]: "a div unit_factor a = normalize a"
+proof (cases "a = 0")
+ case True
+ then show ?thesis by simp
+next
+ case False
+ then have "unit_factor a \<noteq> 0"
+ by simp
+ with nonzero_mult_div_cancel_left
+ have "unit_factor a * normalize a div unit_factor a = normalize a"
+ by blast
+ then show ?thesis by simp
+qed
+
+lemma normalize_div [simp]: "normalize a div a = 1 div unit_factor a"
+proof (cases "a = 0")
+ case True
+ then show ?thesis by simp
+next
+ case False
+ have "normalize a div a = normalize a div (unit_factor a * normalize a)"
+ by simp
+ also have "\<dots> = 1 div unit_factor a"
+ using False by (subst is_unit_div_mult_cancel_right) simp_all
+ finally show ?thesis .
+qed
+
+lemma is_unit_normalize:
assumes "is_unit a"
- shows "unit_factor a = a"
+ shows "normalize a = 1"
proof -
- from assms have "normalize a = 1" by (rule is_unit_normalize)
- moreover from unit_factor_mult_normalize have "unit_factor a * normalize a = a" .
- ultimately show ?thesis by simp
+ from assms have "unit_factor a = a"
+ by (rule is_unit_unit_factor)
+ moreover from assms have "a \<noteq> 0"
+ by auto
+ moreover have "normalize a = a div unit_factor a"
+ by simp
+ ultimately show ?thesis
+ by simp
qed
lemma unit_factor_1 [simp]: "unit_factor 1 = 1"
@@ -1251,32 +1290,6 @@
then show ?thesis by simp
qed
-lemma div_unit_factor [simp]: "a div unit_factor a = normalize a"
-proof (cases "a = 0")
- case True
- then show ?thesis by simp
-next
- case False
- then have "unit_factor a \<noteq> 0" by simp
- with nonzero_mult_div_cancel_left
- have "unit_factor a * normalize a div unit_factor a = normalize a"
- by blast
- then show ?thesis by simp
-qed
-
-lemma normalize_div [simp]: "normalize a div a = 1 div unit_factor a"
-proof (cases "a = 0")
- case True
- then show ?thesis by simp
-next
- case False
- have "normalize a div a = normalize a div (unit_factor a * normalize a)"
- by simp
- also have "\<dots> = 1 div unit_factor a"
- using False by (subst is_unit_div_mult_cancel_right) simp_all
- finally show ?thesis .
-qed
-
lemma mult_one_div_unit_factor [simp]: "a * (1 div unit_factor b) = a div unit_factor b"
by (cases "b = 0") simp_all
@@ -1823,6 +1836,14 @@
proposition abs_eq_iff: "\<bar>x\<bar> = \<bar>y\<bar> \<longleftrightarrow> x = y \<or> x = -y"
by (auto simp add: abs_if split: if_split_asm)
+lemma abs_eq_iff':
+ "\<bar>a\<bar> = b \<longleftrightarrow> b \<ge> 0 \<and> (a = b \<or> a = - b)"
+ by (cases "a \<ge> 0") auto
+
+lemma eq_abs_iff':
+ "a = \<bar>b\<bar> \<longleftrightarrow> a \<ge> 0 \<and> (b = a \<or> b = - a)"
+ using abs_eq_iff' [of b a] by auto
+
lemma sum_squares_ge_zero: "0 \<le> x * x + y * y"
by (intro add_nonneg_nonneg zero_le_square)