--- a/src/HOL/Divides.thy Fri Aug 19 05:49:10 2022 +0000
+++ b/src/HOL/Divides.thy Fri Aug 19 05:49:11 2022 +0000
@@ -62,8 +62,10 @@
text \<open>Enable (lin)arith to deal with \<^const>\<open>divide\<close> and \<^const>\<open>modulo\<close>
when these are applied to some constant that is of the form
\<^term>\<open>numeral k\<close>:\<close>
-declare split_zdiv [of _ _ \<open>numeral k\<close>, linarith_split] for k
-declare split_zmod [of _ _ \<open>numeral k\<close>, linarith_split] for k
+declare split_zdiv [of _ _ \<open>numeral n\<close>, linarith_split] for n
+declare split_zdiv [of _ _ \<open>- numeral n\<close>, linarith_split] for n
+declare split_zmod [of _ _ \<open>numeral n\<close>, linarith_split] for n
+declare split_zmod [of _ _ \<open>- numeral n\<close>, linarith_split] for n
lemma half_nonnegative_int_iff [simp]:
\<open>k div 2 \<ge> 0 \<longleftrightarrow> k \<ge> 0\<close> for k :: int
--- a/src/HOL/Euclidean_Division.thy Fri Aug 19 05:49:10 2022 +0000
+++ b/src/HOL/Euclidean_Division.thy Fri Aug 19 05:49:11 2022 +0000
@@ -1480,6 +1480,9 @@
qed
qed
+declare split_div [of _ _ \<open>numeral n\<close>, linarith_split] for n
+declare split_mod [of _ _ \<open>numeral n\<close>, linarith_split] for n
+
lemma funpow_mod_eq: \<^marker>\<open>contributor \<open>Lars Noschinski\<close>\<close>
\<open>(f ^^ (m mod n)) x = (f ^^ m) x\<close> if \<open>(f ^^ n) x = x\<close>
proof -
--- a/src/HOL/Fields.thy Fri Aug 19 05:49:10 2022 +0000
+++ b/src/HOL/Fields.thy Fri Aug 19 05:49:11 2022 +0000
@@ -13,32 +13,6 @@
imports Nat
begin
-context idom
-begin
-
-lemma inj_mult_left [simp]: \<open>inj ((*) a) \<longleftrightarrow> a \<noteq> 0\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
-proof
- assume ?P
- show ?Q
- proof
- assume \<open>a = 0\<close>
- with \<open>?P\<close> have "inj ((*) 0)"
- by simp
- moreover have "0 * 0 = 0 * 1"
- by simp
- ultimately have "0 = 1"
- by (rule injD)
- then show False
- by simp
- qed
-next
- assume ?Q then show ?P
- by (auto intro: injI)
-qed
-
-end
-
-
subsection \<open>Division rings\<close>
text \<open>
@@ -60,7 +34,7 @@
ML_file \<open>~~/src/Provers/Arith/fast_lin_arith.ML\<close>
ML_file \<open>Tools/lin_arith.ML\<close>
setup \<open>Lin_Arith.global_setup\<close>
-declaration \<open>K (
+declaration \<open>K (
Lin_Arith.init_arith_data
#> Lin_Arith.add_discrete_type \<^type_name>\<open>nat\<close>
#> Lin_Arith.add_lessD @{thm Suc_leI}
@@ -85,7 +59,7 @@
\<^text>\<open>fast_nat_arith_simproc\<close> anyway. However, it seems cheaper to activate the
solver all the time rather than add the additional check.\<close>
-lemmas [linarith_split] = nat_diff_split split_min split_max
+lemmas [linarith_split] = nat_diff_split split_min split_max abs_split
text\<open>Lemmas \<open>divide_simps\<close> move division to the outside and eliminates them on (in)equalities.\<close>
--- a/src/HOL/Int.thy Fri Aug 19 05:49:10 2022 +0000
+++ b/src/HOL/Int.thy Fri Aug 19 05:49:11 2022 +0000
@@ -737,16 +737,6 @@
lemma zadd_int_left: "int m + (int n + z) = int (m + n) + z"
by simp
-text \<open>
- This version is proved for all ordered rings, not just integers!
- It is proved here because attribute \<open>linarith_split\<close> is not available
- in theory \<open>Rings\<close>.
- But is it really better than just rewriting with \<open>abs_if\<close>?
-\<close>
-lemma abs_split [linarith_split, no_atp]: "P \<bar>a\<bar> \<longleftrightarrow> (0 \<le> a \<longrightarrow> P a) \<and> (a < 0 \<longrightarrow> P (- a))"
- for a :: "'a::linordered_idom"
- by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
-
lemma negD:
assumes "x < 0" shows "\<exists>n. x = - (int (Suc n))"
proof -
--- a/src/HOL/Numeral_Simprocs.thy Fri Aug 19 05:49:10 2022 +0000
+++ b/src/HOL/Numeral_Simprocs.thy Fri Aug 19 05:49:11 2022 +0000
@@ -20,9 +20,6 @@
numeral_One [symmetric] uminus_numeral_One [symmetric] Suc_eq_plus1
eq_numeral_iff_iszero not_iszero_Numeral1
-declare split_div [of _ _ "numeral k", linarith_split] for k
-declare split_mod [of _ _ "numeral k", linarith_split] for k
-
text \<open>For \<open>combine_numerals\<close>\<close>
lemma left_add_mult_distrib: "i*u + (j*u + k) = (i+j)*u + (k::nat)"
--- a/src/HOL/Rings.thy Fri Aug 19 05:49:10 2022 +0000
+++ b/src/HOL/Rings.thy Fri Aug 19 05:49:11 2022 +0000
@@ -560,6 +560,26 @@
then show "a * a = b * b" by auto
qed
+lemma inj_mult_left [simp]: \<open>inj ((*) a) \<longleftrightarrow> a \<noteq> 0\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
+proof
+ assume ?P
+ show ?Q
+ proof
+ assume \<open>a = 0\<close>
+ with \<open>?P\<close> have "inj ((*) 0)"
+ by simp
+ moreover have "0 * 0 = 0 * 1"
+ by simp
+ ultimately have "0 = 1"
+ by (rule injD)
+ then show False
+ by simp
+ qed
+next
+ assume ?Q then show ?P
+ by (auto intro: injI)
+qed
+
end
class idom_abs_sgn = idom + abs + sgn +
@@ -2651,6 +2671,12 @@
shows "x+y < 0 \<Longrightarrow> x<0 \<or> y<0"
by (auto simp: not_less intro: le_less_trans [of _ "x+y"])
+text \<open>
+ Is this really better than just rewriting with \<open>abs_if\<close>?
+\<close>
+lemma abs_split [no_atp]: \<open>P \<bar>a\<bar> \<longleftrightarrow> (0 \<le> a \<longrightarrow> P a) \<and> (a < 0 \<longrightarrow> P (- a))\<close>
+ by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
+
end
text \<open>Reasoning about inequalities with division\<close>