# HG changeset patch # User haftmann # Date 1662751715 -7200 # Node ID 98cab94326d4e0e1429681afc8a50ef1fb55d95d # Parent 7ce11c135dad6a419c3198d304979d72d28f31e9 less specialized euclidean relation on int diff -r 7ce11c135dad -r 98cab94326d4 src/HOL/Divides.thy --- 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 \Uniqueness rules\ -inductive eucl_rel_int :: "int \ int \ int \ int \ bool" - where eucl_rel_int_by0: "eucl_rel_int k 0 (0, k)" - | eucl_rel_int_dividesI: "l \ 0 \ k = q * l \ eucl_rel_int k l (q, 0)" - | eucl_rel_int_remainderI: "sgn r = sgn l \ \r\ < \l\ - \ k = q * l + r \ eucl_rel_int k l (q, r)" - -lemma eucl_rel_int_iff: - "eucl_rel_int k l (q, r) \ - k = l * q + r \ - (if 0 < l then 0 \ r \ r < l else if l < 0 then l < r \ r \ 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]: + \(k div l, k mod l) = (q, r)\ + if by0': \l = 0 \ q = 0 \ r = k\ + and divides': \l \ 0 \ l dvd k \ r = 0 \ k = q * l\ + and euclidean_relation': \l \ 0 \ \ l dvd k \ sgn r = sgn l + \ \r\ < \l\ \ k = q * l + r\ 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 \sgn r = sgn l\ \\r\ < \l\\ \k = q * l + r\ + by simp_all + from \sgn r = sgn l\ \l \ 0\ have \division_segment r = division_segment l\ + by (simp add: division_segment_int_def sgn_if split: if_splits) + with \\r\ < \l\\ \k = q * l + r\ + show ?case + by simp qed -lemma unique_quotient: - \q = q'\ if \eucl_rel_int a b (q, r)\ \eucl_rel_int a b (q', r')\ - 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: - \r = r'\ if \eucl_rel_int a b (q, r)\ \eucl_rel_int a b (q', r')\ -proof - - have \q = q'\ - 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 \eucl_rel_int k l (q, r)\ - shows div_int_unique: \k div l = q\ and mod_int_unique: \k mod l = r\ - 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]: + \(k div l, k mod l) = (q, r)\ + if \l = 0 \ q = 0 \ r = k\ + and \l > 0 \ 0 \ r \ r < l \ k = q * l + r\ + and \l < 0 \ l < r \ r \ 0 \ k = q * l + r\ for k l q r :: int + by (cases l \0::int\ rule: linorder_cases) + (auto dest: that) subsubsection \Computing \div\ and \mod\ with shifting\ @@ -487,28 +458,72 @@ with assms show ?thesis by simp qed -lemma pos_eucl_rel_int_mult_2: - assumes "0 \ 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 \ 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\computing div by shifting\ -lemma pos_zdiv_mult_2: "(0::int) \ 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: \(1 + 2 * b) div (2 * a) = b div a\ (is ?Q) + and pos_zmod_mult_2: \(1 + 2 * b) mod (2 * a) = 1 + 2 * (b mod a)\ (is ?R) + if \0 \ a\ for a b :: int +proof - + have \((1 + 2 * b) div (2 * a), (1 + 2 * b) mod (2 * a)) = (b div a, 1 + 2 * (b mod a))\ + proof (cases \2 * a\ \b div a\ \1 + 2 * (b mod a)\ \1 + 2 * b\ rule: euclidean_relation_intI') + case by0 + then show ?case + by simp + next + case pos + then have \a > 0\ + by simp + moreover have \b mod a < a\ + using \a > 0\ by simp + then have \1 + 2 * (b mod a) < 2 * a\ + by simp + moreover have \2 * (b mod a) + a * (2 * (b div a)) = 2 * (b div a * a + b mod a)\ + 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 \ (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: \(1 + 2 * b) div (2 * a) = (b + 1) div a\ (is ?Q) + and neg_zmod_mult_2: \(1 + 2 * b) mod (2 * a) = 2 * ((b + 1) mod a) - 1\ (is ?R) + if \a \ 0\ for a b :: int +proof - + have \((1 + 2 * b) div (2 * a), (1 + 2 * b) mod (2 * a)) = ((b + 1) div a, 2 * ((b + 1) mod a) - 1)\ + proof (cases \2 * a\ \(b + 1) div a\ \2 * ((b + 1) mod a) - 1\ \1 + 2 * b\ 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 \a < 0\ + by simp + moreover have \(b + 1) mod a > a\ + using \a < 0\ by simp + then have \2 * ((b + 1) mod a) > 1 + 2 * a\ + by simp + moreover have \((1 + b) mod a) \ 0\ + using \a < 0\ by simp + then have \2 * ((1 + b) mod a) \ 0\ + by simp + moreover have \2 * ((1 + b) mod a) + a * (2 * ((1 + b) div a)) = + 2 * ((1 + b) div a * a + (1 + b) mod a)\ + 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 \ 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 \ 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)" diff -r 7ce11c135dad -r 98cab94326d4 src/HOL/Library/Signed_Division.thy --- 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: \a smod b \ {- \b\ + 1..\b\ - 1}\ if \b \ 0\ for a b :: int - using that - apply (cases \b > 0\) - 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 \m = nat \a\\ \n = nat \b\\ + then have \\a\ = int m\ \\b\ = int n\ + by simp_all + with that have \n > 0\ + by simp + with signed_modulo_int_def [of a b] \\a\ = int m\ \\b\ = int n\ + 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: "\ 0 \ a; 0 < b \ \ (a :: int) smod b < b" diff -r 7ce11c135dad -r 98cab94326d4 src/HOL/SMT.thy --- 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) \ (B div n)" + \A div n + (if B mod n = 0 then 1 else 0) \ B div n\ + if \A < B\ \0 < n\ + for A B n :: int proof - - have f2: "B div n = A div n \ A div n < B div n" - by (metis (no_types) assms less_le zdiv_mono1) - have "B div n \ A div n \ B mod n \ 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 \ A div n + (if B mod n = 0 then 1 else 0) \ B div n" - using f2 by (auto dest: zless_imp_add1_zle) - then show ?thesis - using assms zdiv_mono1 by auto + from \A < B\ \0 < n\ have \A div n \ B div n\ + by (auto intro: zdiv_mono1) + show ?thesis + proof (cases \n dvd B\) + case False + with \A div n \ B div n\ show ?thesis + by auto + next + case True + then obtain C where \B = n * C\ .. + then have \B div n = C\ + using \0 < n\ by simp + from \0 < n\ have \A mod n \ 0\ + by simp + have \A div n < C\ + proof (rule ccontr) + assume \\ A div n < C\ + then have \C \ A div n\ + by simp + with \B div n = C\ \A div n \ B div n\ + have \A div n = C\ + by simp + moreover from \A < B\ have \n * (A div n) + A mod n < B\ + by simp + ultimately have \n * C + A mod n < n * C\ + using \B = n * C\ by simp + moreover have \A mod n \ 0\ + using \0 < n\ by simp + ultimately show False + by simp + qed + with \n dvd B\ \B div n = C\ show ?thesis + by simp + qed qed - lemma verit_less_mono_div_int2: fixes A B :: int assumes "A \ B" "0 < -n"