# HG changeset patch
# User haftmann
# Date 1660888151 0
# Node ID 714fad33252e41c373ac486309cff7c8621dfcc4
# Parent  24b17460ee60109b43986d610b98d6324a82ec95
more thorough split rules for div and mod on numerals, tuned split rules setup

diff -r 24b17460ee60 -r 714fad33252e src/HOL/Divides.thy
--- 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
diff -r 24b17460ee60 -r 714fad33252e src/HOL/Euclidean_Division.thy
--- 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 -
diff -r 24b17460ee60 -r 714fad33252e src/HOL/Fields.thy
--- 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>
 
diff -r 24b17460ee60 -r 714fad33252e src/HOL/Int.thy
--- 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 -
diff -r 24b17460ee60 -r 714fad33252e src/HOL/Numeral_Simprocs.thy
--- 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)"
diff -r 24b17460ee60 -r 714fad33252e src/HOL/Rings.thy
--- 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>