--- a/src/HOL/Divides.thy Sat Sep 10 15:48:36 2022 +0200
+++ b/src/HOL/Divides.thy Fri Sep 09 21:28:35 2022 +0200
@@ -402,67 +402,38 @@
subsubsection \<open>Uniqueness rules\<close>
-inductive eucl_rel_int :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool"
- where eucl_rel_int_by0: "eucl_rel_int k 0 (0, k)"
- | eucl_rel_int_dividesI: "l \<noteq> 0 \<Longrightarrow> k = q * l \<Longrightarrow> eucl_rel_int k l (q, 0)"
- | eucl_rel_int_remainderI: "sgn r = sgn l \<Longrightarrow> \<bar>r\<bar> < \<bar>l\<bar>
- \<Longrightarrow> k = q * l + r \<Longrightarrow> eucl_rel_int k l (q, r)"
-
-lemma eucl_rel_int_iff:
- "eucl_rel_int k l (q, r) \<longleftrightarrow>
- k = l * q + r \<and>
- (if 0 < l then 0 \<le> r \<and> r < l else if l < 0 then l < r \<and> r \<le> 0 else q = 0)"
- by (cases "r = 0")
- (auto elim!: eucl_rel_int.cases intro: eucl_rel_int_by0 eucl_rel_int_dividesI eucl_rel_int_remainderI
- simp add: ac_simps sgn_1_pos sgn_1_neg)
-
-lemma eucl_rel_int:
- "eucl_rel_int k l (k div l, k mod l)"
-proof (cases k rule: int_cases3)
- case zero
- then show ?thesis
- by (simp add: eucl_rel_int_iff divide_int_def modulo_int_def)
+lemma euclidean_relation_intI [case_names by0 divides euclidean_relation]:
+ \<open>(k div l, k mod l) = (q, r)\<close>
+ if by0': \<open>l = 0 \<Longrightarrow> q = 0 \<and> r = k\<close>
+ and divides': \<open>l \<noteq> 0 \<Longrightarrow> l dvd k \<Longrightarrow> r = 0 \<and> k = q * l\<close>
+ and euclidean_relation': \<open>l \<noteq> 0 \<Longrightarrow> \<not> l dvd k \<Longrightarrow> sgn r = sgn l
+ \<and> \<bar>r\<bar> < \<bar>l\<bar> \<and> k = q * l + r\<close> for k l :: int
+proof (cases l q r k rule: euclidean_relationI)
+ case by0
+ then show ?case
+ by (rule by0')
next
- case (pos n)
- then show ?thesis
- using div_mult_mod_eq [of n]
- by (cases l rule: int_cases3)
- (auto simp del: of_nat_mult of_nat_add
- simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
- eucl_rel_int_iff divide_int_def modulo_int_def)
+ case divides
+ then show ?case
+ by (rule divides')
next
- case (neg n)
- then show ?thesis
- using div_mult_mod_eq [of n]
- by (cases l rule: int_cases3)
- (auto simp del: of_nat_mult of_nat_add
- simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
- eucl_rel_int_iff divide_int_def modulo_int_def)
+ case euclidean_relation
+ with euclidean_relation' have \<open>sgn r = sgn l\<close> \<open>\<bar>r\<bar> < \<bar>l\<bar>\<close> \<open>k = q * l + r\<close>
+ by simp_all
+ from \<open>sgn r = sgn l\<close> \<open>l \<noteq> 0\<close> have \<open>division_segment r = division_segment l\<close>
+ by (simp add: division_segment_int_def sgn_if split: if_splits)
+ with \<open>\<bar>r\<bar> < \<bar>l\<bar>\<close> \<open>k = q * l + r\<close>
+ show ?case
+ by simp
qed
-lemma unique_quotient:
- \<open>q = q'\<close> if \<open>eucl_rel_int a b (q, r)\<close> \<open>eucl_rel_int a b (q', r')\<close>
- apply (rule order_antisym)
- using that
- apply (simp_all add: eucl_rel_int_iff linorder_neq_iff split: if_split_asm)
- apply (blast intro: order_eq_refl [THEN unique_quotient_lemma] order_eq_refl [THEN unique_quotient_lemma_neg] sym)+
- done
-
-lemma unique_remainder:
- \<open>r = r'\<close> if \<open>eucl_rel_int a b (q, r)\<close> \<open>eucl_rel_int a b (q', r')\<close>
-proof -
- have \<open>q = q'\<close>
- using that by (blast intro: unique_quotient)
- then show ?thesis
- using that by (simp add: eucl_rel_int_iff)
-qed
-
-lemma divmod_int_unique:
- assumes \<open>eucl_rel_int k l (q, r)\<close>
- shows div_int_unique: \<open>k div l = q\<close> and mod_int_unique: \<open>k mod l = r\<close>
- using assms eucl_rel_int [of k l]
- using unique_quotient [of k l] unique_remainder [of k l]
- by auto
+lemma euclidean_relation_intI' [case_names by0 pos neg]:
+ \<open>(k div l, k mod l) = (q, r)\<close>
+ if \<open>l = 0 \<Longrightarrow> q = 0 \<and> r = k\<close>
+ and \<open>l > 0 \<Longrightarrow> 0 \<le> r \<and> r < l \<and> k = q * l + r\<close>
+ and \<open>l < 0 \<Longrightarrow> l < r \<and> r \<le> 0 \<and> k = q * l + r\<close> for k l q r :: int
+ by (cases l \<open>0::int\<close> rule: linorder_cases)
+ (auto dest: that)
subsubsection \<open>Computing \<open>div\<close> and \<open>mod\<close> with shifting\<close>
@@ -487,28 +458,72 @@
with assms show ?thesis by simp
qed
-lemma pos_eucl_rel_int_mult_2:
- assumes "0 \<le> b"
- assumes "eucl_rel_int a b (q, r)"
- shows "eucl_rel_int (1 + 2*a) (2*b) (q, 1 + 2*r)"
- using assms unfolding eucl_rel_int_iff by auto
-
-lemma neg_eucl_rel_int_mult_2:
- assumes "b \<le> 0"
- assumes "eucl_rel_int (a + 1) b (q, r)"
- shows "eucl_rel_int (1 + 2*a) (2*b) (q, 2*r - 1)"
- using assms unfolding eucl_rel_int_iff by auto
-
text\<open>computing div by shifting\<close>
-lemma pos_zdiv_mult_2: "(0::int) \<le> a ==> (1 + 2*b) div (2*a) = b div a"
- using pos_eucl_rel_int_mult_2 [OF _ eucl_rel_int]
- by (rule div_int_unique)
+lemma pos_zdiv_mult_2: \<open>(1 + 2 * b) div (2 * a) = b div a\<close> (is ?Q)
+ and pos_zmod_mult_2: \<open>(1 + 2 * b) mod (2 * a) = 1 + 2 * (b mod a)\<close> (is ?R)
+ if \<open>0 \<le> a\<close> for a b :: int
+proof -
+ have \<open>((1 + 2 * b) div (2 * a), (1 + 2 * b) mod (2 * a)) = (b div a, 1 + 2 * (b mod a))\<close>
+ proof (cases \<open>2 * a\<close> \<open>b div a\<close> \<open>1 + 2 * (b mod a)\<close> \<open>1 + 2 * b\<close> rule: euclidean_relation_intI')
+ case by0
+ then show ?case
+ by simp
+ next
+ case pos
+ then have \<open>a > 0\<close>
+ by simp
+ moreover have \<open>b mod a < a\<close>
+ using \<open>a > 0\<close> by simp
+ then have \<open>1 + 2 * (b mod a) < 2 * a\<close>
+ by simp
+ moreover have \<open>2 * (b mod a) + a * (2 * (b div a)) = 2 * (b div a * a + b mod a)\<close>
+ by (simp only: algebra_simps)
+ ultimately show ?case
+ by (simp add: algebra_simps)
+ next
+ case neg
+ with that show ?case
+ by simp
+ qed
+ then show ?Q and ?R
+ by simp_all
+qed
-lemma neg_zdiv_mult_2:
- assumes A: "a \<le> (0::int)" shows "(1 + 2*b) div (2*a) = (b+1) div a"
- using neg_eucl_rel_int_mult_2 [OF A eucl_rel_int]
- by (rule div_int_unique)
+lemma neg_zdiv_mult_2: \<open>(1 + 2 * b) div (2 * a) = (b + 1) div a\<close> (is ?Q)
+ and neg_zmod_mult_2: \<open>(1 + 2 * b) mod (2 * a) = 2 * ((b + 1) mod a) - 1\<close> (is ?R)
+ if \<open>a \<le> 0\<close> for a b :: int
+proof -
+ have \<open>((1 + 2 * b) div (2 * a), (1 + 2 * b) mod (2 * a)) = ((b + 1) div a, 2 * ((b + 1) mod a) - 1)\<close>
+ proof (cases \<open>2 * a\<close> \<open>(b + 1) div a\<close> \<open>2 * ((b + 1) mod a) - 1\<close> \<open>1 + 2 * b\<close> rule: euclidean_relation_intI')
+ case by0
+ then show ?case
+ by simp
+ next
+ case pos
+ with that show ?case
+ by simp
+ next
+ case neg
+ then have \<open>a < 0\<close>
+ by simp
+ moreover have \<open>(b + 1) mod a > a\<close>
+ using \<open>a < 0\<close> by simp
+ then have \<open>2 * ((b + 1) mod a) > 1 + 2 * a\<close>
+ by simp
+ moreover have \<open>((1 + b) mod a) \<le> 0\<close>
+ using \<open>a < 0\<close> by simp
+ then have \<open>2 * ((1 + b) mod a) \<le> 0\<close>
+ by simp
+ moreover have \<open>2 * ((1 + b) mod a) + a * (2 * ((1 + b) div a)) =
+ 2 * ((1 + b) div a * a + (1 + b) mod a)\<close>
+ by (simp only: algebra_simps)
+ ultimately show ?case
+ by (simp add: algebra_simps)
+ qed
+ then show ?Q and ?R
+ by simp_all
+qed
lemma zdiv_numeral_Bit0 [simp]:
"numeral (Num.Bit0 v) div numeral (Num.Bit0 w) =
@@ -523,20 +538,6 @@
unfolding mult_2 [symmetric] add.commute [of _ 1]
by (rule pos_zdiv_mult_2, simp)
-lemma pos_zmod_mult_2:
- fixes a b :: int
- assumes "0 \<le> a"
- shows "(1 + 2 * b) mod (2 * a) = 1 + 2 * (b mod a)"
- using pos_eucl_rel_int_mult_2 [OF assms eucl_rel_int]
- by (rule mod_int_unique)
-
-lemma neg_zmod_mult_2:
- fixes a b :: int
- assumes "a \<le> 0"
- shows "(1 + 2 * b) mod (2 * a) = 2 * ((b + 1) mod a) - 1"
- using neg_eucl_rel_int_mult_2 [OF assms eucl_rel_int]
- by (rule mod_int_unique)
-
lemma zmod_numeral_Bit0 [simp]:
"numeral (Num.Bit0 v) mod numeral (Num.Bit0 w) =
(2::int) * (numeral v mod numeral w)"
--- a/src/HOL/Library/Signed_Division.thy Sat Sep 10 15:48:36 2022 +0200
+++ b/src/HOL/Library/Signed_Division.thy Fri Sep 09 21:28:35 2022 +0200
@@ -147,20 +147,16 @@
lemma smod_int_range:
\<open>a smod b \<in> {- \<bar>b\<bar> + 1..\<bar>b\<bar> - 1}\<close>
if \<open>b \<noteq> 0\<close> for a b :: int
- using that
- apply (cases \<open>b > 0\<close>)
- apply (insert pos_mod_conj [where a=a and b=b])[1]
- apply (insert pos_mod_conj [where a="-a" and b=b])[1]
- apply (auto simp: smod_int_alt_def algebra_simps sgn_if
- abs_if not_less add1_zle_eq [simplified add.commute])[1]
- apply (metis add_nonneg_nonneg int_one_le_iff_zero_less le_less less_add_same_cancel2 not_le pos_mod_conj)
- apply (metis (full_types) add.inverse_inverse eucl_rel_int eucl_rel_int_iff le_less_trans neg_0_le_iff_le)
- apply (insert neg_mod_conj [where a=a and b="b"])[1]
- apply (insert neg_mod_conj [where a="-a" and b="b"])[1]
- apply (clarsimp simp: smod_int_alt_def algebra_simps sgn_if
- abs_if not_less add1_zle_eq [simplified add.commute])
- apply (metis neg_0_less_iff_less neg_mod_conj not_le not_less_iff_gr_or_eq order_trans pos_mod_conj)
- done
+proof -
+ define m n where \<open>m = nat \<bar>a\<bar>\<close> \<open>n = nat \<bar>b\<bar>\<close>
+ then have \<open>\<bar>a\<bar> = int m\<close> \<open>\<bar>b\<bar> = int n\<close>
+ by simp_all
+ with that have \<open>n > 0\<close>
+ by simp
+ with signed_modulo_int_def [of a b] \<open>\<bar>a\<bar> = int m\<close> \<open>\<bar>b\<bar> = int n\<close>
+ show ?thesis
+ by (auto simp add: sgn_if diff_le_eq int_one_le_iff_zero_less simp flip: of_nat_mod of_nat_diff)
+qed
lemma smod_int_compares:
"\<lbrakk> 0 \<le> a; 0 < b \<rbrakk> \<Longrightarrow> (a :: int) smod b < b"
--- a/src/HOL/SMT.thy Sat Sep 10 15:48:36 2022 +0200
+++ b/src/HOL/SMT.thy Fri Sep 09 21:28:35 2022 +0200
@@ -520,22 +520,46 @@
qed
lemma verit_le_mono_div_int:
- fixes A B :: int
- assumes "A < B" "0 < n"
- shows "(A div n) + (if B mod n = 0 then 1 else 0) \<le> (B div n)"
+ \<open>A div n + (if B mod n = 0 then 1 else 0) \<le> B div n\<close>
+ if \<open>A < B\<close> \<open>0 < n\<close>
+ for A B n :: int
proof -
- have f2: "B div n = A div n \<or> A div n < B div n"
- by (metis (no_types) assms less_le zdiv_mono1)
- have "B div n \<noteq> A div n \<or> B mod n \<noteq> 0"
- using assms(1) by (metis Groups.add_ac(2) assms(2) eucl_rel_int eucl_rel_int_iff
- group_cancel.rule0 le_add_same_cancel2 not_le)
- then have "B mod n = 0 \<longrightarrow> A div n + (if B mod n = 0 then 1 else 0) \<le> B div n"
- using f2 by (auto dest: zless_imp_add1_zle)
- then show ?thesis
- using assms zdiv_mono1 by auto
+ from \<open>A < B\<close> \<open>0 < n\<close> have \<open>A div n \<le> B div n\<close>
+ by (auto intro: zdiv_mono1)
+ show ?thesis
+ proof (cases \<open>n dvd B\<close>)
+ case False
+ with \<open>A div n \<le> B div n\<close> show ?thesis
+ by auto
+ next
+ case True
+ then obtain C where \<open>B = n * C\<close> ..
+ then have \<open>B div n = C\<close>
+ using \<open>0 < n\<close> by simp
+ from \<open>0 < n\<close> have \<open>A mod n \<ge> 0\<close>
+ by simp
+ have \<open>A div n < C\<close>
+ proof (rule ccontr)
+ assume \<open>\<not> A div n < C\<close>
+ then have \<open>C \<le> A div n\<close>
+ by simp
+ with \<open>B div n = C\<close> \<open>A div n \<le> B div n\<close>
+ have \<open>A div n = C\<close>
+ by simp
+ moreover from \<open>A < B\<close> have \<open>n * (A div n) + A mod n < B\<close>
+ by simp
+ ultimately have \<open>n * C + A mod n < n * C\<close>
+ using \<open>B = n * C\<close> by simp
+ moreover have \<open>A mod n \<ge> 0\<close>
+ using \<open>0 < n\<close> by simp
+ ultimately show False
+ by simp
+ qed
+ with \<open>n dvd B\<close> \<open>B div n = C\<close> show ?thesis
+ by simp
+ qed
qed
-
lemma verit_less_mono_div_int2:
fixes A B :: int
assumes "A \<le> B" "0 < -n"