# HG changeset patch # User wenzelm # Date 1661024095 -7200 # Node ID 06eb4d0031e32b36419341b1b5fa8ce96b92b7ff # Parent d7e0b6620c07dbaea29b1d9d11f2d6fbba22f69d# Parent 4586e90573acaf96b798dbca4ac6df31dc540e06 merged; diff -r 4586e90573ac -r 06eb4d0031e3 NEWS --- a/NEWS Sat Aug 20 21:33:51 2022 +0200 +++ b/NEWS Sat Aug 20 21:34:55 2022 +0200 @@ -34,12 +34,15 @@ *** HOL *** +* Renamed attribute "arith_split" to "linarith_split". Minor +INCOMPATIBILITY. + * Theory Char_ord: streamlined logical specifications. Minor INCOMPATIBILITY. * New Theory Code_Abstract_Char implements characters by target language integers, sacrificing pattern patching in exchange for dramatically -increased performance for comparisions. +increased performance for comparisons. * New theory HOL-Library.NList of fixed length lists @@ -49,6 +52,9 @@ * Theory "HOL.Bit_Operations": rule bit_0 is not default [simp] any longer. INCOMPATIBILITY. +* Streamlined primitive definitions of division and modulus on integers. +INCOMPATIBILITY. + * Theory "HOL.Fun": - Added predicate monotone_on and redefined monotone to be an abbreviation. Lemma monotone_def is explicitly provided for backward @@ -146,6 +152,8 @@ - Added support for TX0 and TX1 TPTP formats and $ite/$let expressions in TH0 and TH1. - Added support for cvc5. + - Generate Isar proofs by default when and only when the one-liner proof + fails to replay and the Isar proof succeeds. - Replaced option "sledgehammer_atp_dest_dir" by "sledgehammer_atp_problem_dest_dir", for problem files, and "sledgehammer_atp_proof_dest_dir", for proof files. Minor INCOMPATIBILITY. diff -r 4586e90573ac -r 06eb4d0031e3 src/Doc/Isar_Ref/HOL_Specific.thy --- a/src/Doc/Isar_Ref/HOL_Specific.thy Sat Aug 20 21:33:51 2022 +0200 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy Sat Aug 20 21:34:55 2022 +0200 @@ -2003,7 +2003,7 @@ \begin{matharray}{rcl} @{method_def (HOL) arith} & : & \method\ \\ @{attribute_def (HOL) arith} & : & \attribute\ \\ - @{attribute_def (HOL) arith_split} & : & \attribute\ \\ + @{attribute_def (HOL) linarith_split} & : & \attribute\ \\ \end{matharray} \<^descr> @{method (HOL) arith} decides linear arithmetic problems (on types \nat\, @@ -2013,7 +2013,7 @@ \<^descr> @{attribute (HOL) arith} declares facts that are supplied to the arithmetic provers implicitly. - \<^descr> @{attribute (HOL) arith_split} attribute declares case split rules to be + \<^descr> @{attribute (HOL) linarith_split} attribute declares case split rules to be expanded before @{method (HOL) arith} is invoked. diff -r 4586e90573ac -r 06eb4d0031e3 src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Sat Aug 20 21:33:51 2022 +0200 +++ b/src/Doc/Sledgehammer/document/root.tex Sat Aug 20 21:34:55 2022 +0200 @@ -1129,9 +1129,9 @@ \opsmart{isar\_proofs}{no\_isar\_proofs} Specifies whether Isar proofs should be output in addition to one-line proofs. The construction of Isar proof is still experimental and may sometimes fail; -however, when they succeed they are usually faster and more intelligible than -one-line proofs. If the option is set to \textit{smart} (the default), Isar -proofs are only generated when no working one-line proof is available. +however, when they succeed they can be faster and sometimes more intelligible +than one-line proofs. If the option is set to \textit{smart} (the default), Isar +proofs are generated only when no working one-line proof is available. \opdefault{compress}{int}{smart} Specifies the granularity of the generated Isar proofs if \textit{isar\_proofs} @@ -1191,14 +1191,13 @@ Specifies the maximum number of seconds that the automatic provers should spend searching for a proof. This excludes problem preparation and is a soft limit. -\opdefault{slices}{int}{\upshape 6 times the number of cores detected} -Specifies the number of time slices. Each time slice corresponds to a prover -invocation and has its own set of options. For example, for SPASS, one slice -might specify the fast but incomplete set-of-support (SOS) strategy with 100 -relevant lemmas, whereas other slices might run without SOS and with 500 lemmas. -Slicing (and thereby parallelism) can be disable by setting \textit{slices} to -1. Since slicing is a valuable optimization, you should probably leave it -enabled unless you are conducting experiments. +\opdefault{slices}{int}{\upshape 12 times the number of cores detected} +Specifies the number of time slices. Time slices are the basic unit for prover +invocations. They are divided among the available provers. A single prover +invocation can occupy a single slice, two slices, or more, depending on the +prover. Slicing (and thereby parallelism) can be disable by setting +\textit{slices} to 1. Since slicing is a valuable optimization, you should +probably leave it enabled unless you are conducting experiments. \nopagebreak {\small See also \textit{verbose} (\S\ref{output-format}).} diff -r 4586e90573ac -r 06eb4d0031e3 src/HOL/Archimedean_Field.thy --- a/src/HOL/Archimedean_Field.thy Sat Aug 20 21:33:51 2022 +0200 +++ b/src/HOL/Archimedean_Field.thy Sat Aug 20 21:34:55 2022 +0200 @@ -243,7 +243,7 @@ lemma floor_le_iff: "\x\ \ z \ x < of_int z + 1" by (simp add: not_less [symmetric] less_floor_iff) -lemma floor_split[arith_split]: "P \t\ \ (\i. of_int i \ t \ t < of_int i + 1 \ P i)" +lemma floor_split[linarith_split]: "P \t\ \ (\i. of_int i \ t \ t < of_int i + 1 \ P i)" by (metis floor_correct floor_unique less_floor_iff not_le order_refl) lemma floor_mono: @@ -618,7 +618,7 @@ lemma ceiling_diff_one [simp]: "\x - 1\ = \x\ - 1" using ceiling_diff_of_int [of x 1] by simp -lemma ceiling_split[arith_split]: "P \t\ \ (\i. of_int i - 1 < t \ t \ of_int i \ P i)" +lemma ceiling_split[linarith_split]: "P \t\ \ (\i. of_int i - 1 < t \ t \ of_int i \ P i)" by (auto simp add: ceiling_unique ceiling_correct) lemma ceiling_diff_floor_le_1: "\x\ - \x\ \ 1" diff -r 4586e90573ac -r 06eb4d0031e3 src/HOL/Bit_Operations.thy --- a/src/HOL/Bit_Operations.thy Sat Aug 20 21:33:51 2022 +0200 +++ b/src/HOL/Bit_Operations.thy Sat Aug 20 21:34:55 2022 +0200 @@ -1465,7 +1465,7 @@ lemma not_int_div_2: \NOT k div 2 = NOT (k div 2)\ for k :: int - by (cases k) (simp_all add: not_int_def divide_int_def nat_add_distrib) + by (simp add: not_int_def) lemma bit_not_int_iff: \bit (NOT k) n \ \ bit k n\ @@ -1729,7 +1729,7 @@ case (odd k) from odd.IH [of \l div 2\] odd.hyps odd.prems show ?case - by (simp add: and_int_rec [of _ l]) linarith + by (simp add: and_int_rec [of _ l]) qed lemma or_nonnegative_int_iff [simp]: @@ -1754,7 +1754,7 @@ case (even k) from even.IH [of \l div 2\] even.hyps even.prems show ?case - by (simp add: or_int_rec [of _ l]) linarith + by (simp add: or_int_rec [of _ l]) next case (odd k) from odd.IH [of \l div 2\] odd.hyps odd.prems @@ -2173,22 +2173,6 @@ \\ 2 ^ n \ (0::int)\ by (simp add: power_le_zero_eq) -lemma half_nonnegative_int_iff [simp]: - \k div 2 \ 0 \ k \ 0\ for k :: int -proof (cases \k \ 0\) - case True - then show ?thesis - by (auto simp add: divide_int_def sgn_1_pos) -next - case False - then show ?thesis - by (auto simp add: divide_int_def not_le elim!: evenE) -qed - -lemma half_negative_int_iff [simp]: - \k div 2 < 0 \ k < 0\ for k :: int - by (subst Not_eq_iff [symmetric]) (simp add: not_less) - lemma int_bit_bound: fixes k :: int obtains n where \\m. n \ m \ bit k m \ bit k n\ diff -r 4586e90573ac -r 06eb4d0031e3 src/HOL/Code_Numeral.thy --- a/src/HOL/Code_Numeral.thy Sat Aug 20 21:33:51 2022 +0200 +++ b/src/HOL/Code_Numeral.thy Sat Aug 20 21:34:55 2022 +0200 @@ -385,17 +385,17 @@ where divmod_integer'_def: "divmod_integer m n = (numeral m div numeral n, numeral m mod numeral n)" -definition divmod_step_integer :: "num \ integer \ integer \ integer \ integer" +definition divmod_step_integer :: "integer \ integer \ integer \ integer \ integer" where "divmod_step_integer l qr = (let (q, r) = qr - in if r \ numeral l then (2 * q + 1, r - numeral l) + in if r \ l then (2 * q + 1, r - l) else (2 * q, r))" instance proof show "divmod m n = (numeral m div numeral n :: integer, numeral m mod numeral n)" for m n by (fact divmod_integer'_def) show "divmod_step l qr = (let (q, r) = qr - in if r \ numeral l then (2 * q + 1, r - numeral l) + in if r \ l then (2 * q + 1, r - l) else (2 * q, r))" for l and qr :: "integer \ integer" by (fact divmod_step_integer_def) qed (transfer, diff -r 4586e90573ac -r 06eb4d0031e3 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Sat Aug 20 21:33:51 2022 +0200 +++ b/src/HOL/Divides.thy Sat Aug 20 21:34:55 2022 +0200 @@ -11,19 +11,7 @@ subsection \More on division\ -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) +subsubsection \Monotonicity in the First Argument (Dividend)\ lemma unique_quotient_lemma: assumes "b * q' + r' \ b * q + r" "0 \ r'" "r' < b" "r < b" shows "q' \ (q::int)" @@ -42,188 +30,14 @@ "b * q' + r' \ b*q + r \ r \ 0 \ b < r \ b < r' \ q \ (q'::int)" using unique_quotient_lemma[where b = "-b" and r = "-r'" and r'="-r"] by auto -lemma unique_quotient: - "eucl_rel_int a b (q, r) \ eucl_rel_int a b (q', r') \ q = q'" - apply (rule order_antisym) - 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: - assumes "eucl_rel_int a b (q, r)" - and "eucl_rel_int a b (q', r')" - shows "r = r'" -proof - - have "q = q'" - using assms by (blast intro: unique_quotient) - then show "r = r'" - using assms by (simp add: eucl_rel_int_iff) -qed - -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) -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) -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) -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 div_abs_eq_div_nat: - "\k\ div \l\ = int (nat \k\ div nat \l\)" - by (simp add: divide_int_def) - -lemma mod_abs_eq_div_nat: - "\k\ mod \l\ = int (nat \k\ mod nat \l\)" - by (simp add: modulo_int_def) - -lemma zdiv_int: - "int (a div b) = int a div int b" - by (simp add: divide_int_def) - -lemma zmod_int: - "int (a mod b) = int a mod int b" - by (simp add: modulo_int_def) - -lemma div_sgn_abs_cancel: - fixes k l v :: int - assumes "v \ 0" - shows "(sgn v * \k\) div (sgn v * \l\) = \k\ div \l\" -proof - - from assms have "sgn v = - 1 \ sgn v = 1" - by (cases "v \ 0") auto - then show ?thesis - using assms unfolding divide_int_def [of "sgn v * \k\" "sgn v * \l\"] - by (fastforce simp add: not_less div_abs_eq_div_nat) -qed - -lemma div_eq_sgn_abs: - fixes k l v :: int - assumes "sgn k = sgn l" - shows "k div l = \k\ div \l\" -proof (cases "l = 0") - case True - then show ?thesis - by simp -next - case False - with assms have "(sgn k * \k\) div (sgn l * \l\) = \k\ div \l\" - using div_sgn_abs_cancel [of l k l] by simp - then show ?thesis - by (simp add: sgn_mult_abs) -qed - -lemma div_dvd_sgn_abs: - fixes k l :: int - assumes "l dvd k" - shows "k div l = (sgn k * sgn l) * (\k\ div \l\)" -proof (cases "k = 0 \ l = 0") - case True - then show ?thesis - by auto -next - case False - then have "k \ 0" and "l \ 0" - by auto - show ?thesis - proof (cases "sgn l = sgn k") - case True - then show ?thesis - by (auto simp add: div_eq_sgn_abs) - next - case False - with \k \ 0\ \l \ 0\ - have "sgn l * sgn k = - 1" - by (simp add: sgn_if split: if_splits) - with assms show ?thesis - unfolding divide_int_def [of k l] - by (auto simp add: zdiv_int ac_simps) - qed -qed - -lemma div_noneq_sgn_abs: - fixes k l :: int - assumes "l \ 0" - assumes "sgn k \ sgn l" - shows "k div l = - (\k\ div \l\) - of_bool (\ l dvd k)" - using assms - by (simp only: divide_int_def [of k l], auto simp add: not_less zdiv_int) - - -subsubsection \Laws for div and mod with Unary Minus\ - -lemma zminus1_lemma: - "eucl_rel_int a b (q, r) ==> b \ 0 - ==> eucl_rel_int (-a) b (if r=0 then -q else -q - 1, - if r=0 then 0 else b-r)" -by (force simp add: eucl_rel_int_iff right_diff_distrib) - - -lemma zdiv_zminus1_eq_if: - "b \ (0::int) - \ (-a) div b = (if a mod b = 0 then - (a div b) else - (a div b) - 1)" -by (blast intro: eucl_rel_int [THEN zminus1_lemma, THEN div_int_unique]) - -lemma zmod_zminus1_eq_if: - "(-a::int) mod b = (if a mod b = 0 then 0 else b - (a mod b))" -proof (cases "b = 0") - case False - then show ?thesis - by (blast intro: eucl_rel_int [THEN zminus1_lemma, THEN mod_int_unique]) -qed auto - -lemma zmod_zminus1_not_zero: - fixes k l :: int - shows "- k mod l \ 0 \ k mod l \ 0" - by (simp add: mod_eq_0_iff_dvd) - -lemma zmod_zminus2_not_zero: - fixes k l :: int - shows "k mod - l \ 0 \ k mod l \ 0" - by (simp add: mod_eq_0_iff_dvd) - -lemma zdiv_zminus2_eq_if: - "b \ (0::int) - ==> a div (-b) = - (if a mod b = 0 then - (a div b) else - (a div b) - 1)" - by (auto simp add: zdiv_zminus1_eq_if div_minus_right) - -lemma zmod_zminus2_eq_if: - "a mod (-b::int) = (if a mod b = 0 then 0 else (a mod b) - b)" - by (auto simp add: zmod_zminus1_eq_if mod_minus_right) - - -subsubsection \Monotonicity in the First Argument (Dividend)\ - lemma zdiv_mono1: - fixes b::int - assumes "a \ a'" "0 < b" shows "a div b \ a' div b" + \a div b \ a' div b\ + if \a \ a'\ \0 < b\ + for a b b' :: int proof (rule unique_quotient_lemma) show "b * (a div b) + a mod b \ b * (a' div b) + a' mod b" - using assms(1) by auto -qed (use assms in auto) + using \a \ a'\ by auto +qed (use that in auto) lemma zdiv_mono1_neg: fixes b::int @@ -299,6 +113,72 @@ by simp qed (use assms in auto) + +subsubsection \Computing \div\ and \mod\ with shifting\ + +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 unique_quotient: + "eucl_rel_int a b (q, r) \ eucl_rel_int a b (q', r') \ q = q'" + apply (rule order_antisym) + 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: + assumes "eucl_rel_int a b (q, r)" + and "eucl_rel_int a b (q', r')" + shows "r = r'" +proof - + have "q = q'" + using assms by (blast intro: unique_quotient) + then show "r = r'" + using assms by (simp add: eucl_rel_int_iff) +qed + +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) +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) +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) +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 div_pos_geq: fixes k l :: int assumes "0 < l" and "l \ k" @@ -319,54 +199,6 @@ with assms show ?thesis by simp qed - -subsubsection \Splitting Rules for div and mod\ - -text\The proofs of the two lemmas below are essentially identical\ - -lemma split_pos_lemma: - "0 - P(n div k :: int)(n mod k) = (\i j. 0\j \ j n = k*i + j \ P i j)" - by auto - -lemma split_neg_lemma: - "k<0 \ - P(n div k :: int)(n mod k) = (\i j. k j\0 \ n = k*i + j \ P i j)" - by auto - -lemma split_zdiv: - "P(n div k :: int) = - ((k = 0 \ P 0) \ - (0 (\i j. 0\j \ j n = k*i + j \ P i)) \ - (k<0 \ (\i j. k j\0 \ n = k*i + j \ P i)))" -proof (cases "k = 0") - case False - then show ?thesis - unfolding linorder_neq_iff - by (auto simp add: split_pos_lemma [of concl: "\x y. P x"] split_neg_lemma [of concl: "\x y. P x"]) -qed auto - -lemma split_zmod: - "P(n mod k :: int) = - ((k = 0 \ P n) \ - (0 (\i j. 0\j \ j n = k*i + j \ P j)) \ - (k<0 \ (\i j. k j\0 \ n = k*i + j \ P j)))" -proof (cases "k = 0") - case False - then show ?thesis - unfolding linorder_neq_iff - by (auto simp add: split_pos_lemma [of concl: "\x y. P y"] split_neg_lemma [of concl: "\x y. P y"]) -qed auto - -text \Enable (lin)arith to deal with \<^const>\divide\ and \<^const>\modulo\ - when these are applied to some constant that is of the form - \<^term>\numeral k\:\ -declare split_zdiv [of _ _ "numeral k", arith_split] for k -declare split_zmod [of _ _ "numeral k", arith_split] for k - - -subsubsection \Computing \div\ and \mod\ with shifting\ - lemma pos_eucl_rel_int_mult_2: assumes "0 \ b" assumes "eucl_rel_int a b (q, r)" @@ -430,31 +262,6 @@ unfolding mult_2 [symmetric] add.commute [of _ 1] by (rule pos_zmod_mult_2, simp) -lemma zdiv_eq_0_iff: - "i div k = 0 \ k = 0 \ 0 \ i \ i < k \ i \ 0 \ k < i" (is "?L = ?R") - for i k :: int -proof - assume ?L - moreover have "?L \ ?R" - by (rule split_zdiv [THEN iffD2]) simp - ultimately show ?R - by blast -next - assume ?R then show ?L - by auto -qed - -lemma zmod_trivial_iff: - fixes i k :: int - shows "i mod k = i \ k = 0 \ 0 \ i \ i < k \ i \ 0 \ k < i" -proof - - have "i mod k = i \ i div k = 0" - using div_mult_mod_eq [of i k] by safe auto - with zdiv_eq_0_iff - show ?thesis - by simp -qed - subsubsection \Quotients of Signs\ @@ -541,7 +348,6 @@ "0 0 < (i::int) div k \ k \ i" using pos_imp_zdiv_nonneg_iff[of k i] zdiv_eq_0_iff[of i k] by arith - lemma neg_imp_zdiv_nonneg_iff: fixes a::int assumes "b < 0" @@ -574,6 +380,28 @@ lemma zmod_le_nonneg_dividend: "(m::int) \ 0 \ m mod k \ m" by (rule split_zmod[THEN iffD2]) (fastforce dest: q_pos_lemma intro: split_mult_pos_le) +lemma sgn_div_eq_sgn_mult: + \sgn (k div l) = of_bool (k div l \ 0) * sgn (k * l)\ + for k l :: int +proof (cases \k div l = 0\) + case True + then show ?thesis + by simp +next + case False + have \0 \ \k\ div \l\\ + by (cases \l = 0\) (simp_all add: pos_imp_zdiv_nonneg_iff) + then have \\k\ div \l\ \ 0 \ 0 < \k\ div \l\\ + by (simp add: less_le) + also have \\ \ \k\ \ \l\\ + using False nonneg1_imp_zdiv_pos_iff by auto + finally have *: \\k\ div \l\ \ 0 \ \l\ \ \k\\ . + show ?thesis + using \0 \ \k\ div \l\\ False + by (auto simp add: div_eq_div_abs [of k l] div_eq_sgn_abs [of k l] + sgn_mult sgn_1_pos sgn_1_neg sgn_eq_0_iff nonneg1_imp_zdiv_pos_iff * dest: sgn_not_eq_imp) +qed + subsubsection \Further properties\ @@ -734,10 +562,10 @@ and div_mult2_eq: "0 \ c \