# HG changeset patch
# User haftmann
# Date 1660888149 0
# Node ID fcd118d9242f8a1343aa2dddeeed50af68c82c7a
# Parent  dc758531077b3f9111c01d4f6514b6d0998bb5a2
consolidated attribute name

diff -r dc758531077b -r fcd118d9242f NEWS
--- a/NEWS	Fri Aug 19 05:49:07 2022 +0000
+++ b/NEWS	Fri Aug 19 05:49:09 2022 +0000
@@ -34,6 +34,9 @@
 
 *** HOL ***
 
+* Renamed attribute "arith_split" to "linarith_split".  Minor
+INCOMPATIBILITY.
+
 * Theory Char_ord: streamlined logical specifications.
 Minor INCOMPATIBILITY.
 
diff -r dc758531077b -r fcd118d9242f src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Fri Aug 19 05:49:07 2022 +0000
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Fri Aug 19 05:49:09 2022 +0000
@@ -2003,7 +2003,7 @@
   \begin{matharray}{rcl}
     @{method_def (HOL) arith} & : & \<open>method\<close> \\
     @{attribute_def (HOL) arith} & : & \<open>attribute\<close> \\
-    @{attribute_def (HOL) arith_split} & : & \<open>attribute\<close> \\
+    @{attribute_def (HOL) linarith_split} & : & \<open>attribute\<close> \\
   \end{matharray}
 
   \<^descr> @{method (HOL) arith} decides linear arithmetic problems (on types \<open>nat\<close>,
@@ -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 dc758531077b -r fcd118d9242f src/HOL/Archimedean_Field.thy
--- a/src/HOL/Archimedean_Field.thy	Fri Aug 19 05:49:07 2022 +0000
+++ b/src/HOL/Archimedean_Field.thy	Fri Aug 19 05:49:09 2022 +0000
@@ -243,7 +243,7 @@
 lemma floor_le_iff: "\<lfloor>x\<rfloor> \<le> z \<longleftrightarrow> x < of_int z + 1"
   by (simp add: not_less [symmetric] less_floor_iff)
 
-lemma floor_split[arith_split]: "P \<lfloor>t\<rfloor> \<longleftrightarrow> (\<forall>i. of_int i \<le> t \<and> t < of_int i + 1 \<longrightarrow> P i)"
+lemma floor_split[linarith_split]: "P \<lfloor>t\<rfloor> \<longleftrightarrow> (\<forall>i. of_int i \<le> t \<and> t < of_int i + 1 \<longrightarrow> 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]: "\<lceil>x - 1\<rceil> = \<lceil>x\<rceil> - 1"
   using ceiling_diff_of_int [of x 1] by simp
 
-lemma ceiling_split[arith_split]: "P \<lceil>t\<rceil> \<longleftrightarrow> (\<forall>i. of_int i - 1 < t \<and> t \<le> of_int i \<longrightarrow> P i)"
+lemma ceiling_split[linarith_split]: "P \<lceil>t\<rceil> \<longleftrightarrow> (\<forall>i. of_int i - 1 < t \<and> t \<le> of_int i \<longrightarrow> P i)"
   by (auto simp add: ceiling_unique ceiling_correct)
 
 lemma ceiling_diff_floor_le_1: "\<lceil>x\<rceil> - \<lfloor>x\<rfloor> \<le> 1"
diff -r dc758531077b -r fcd118d9242f src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Fri Aug 19 05:49:07 2022 +0000
+++ b/src/HOL/Divides.thy	Fri Aug 19 05:49:09 2022 +0000
@@ -62,8 +62,8 @@
 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>, arith_split] for k
-declare split_zmod [of _ _ \<open>numeral k\<close>, arith_split] for k
+declare split_zdiv [of _ _ \<open>numeral k\<close>, linarith_split] for k
+declare split_zmod [of _ _ \<open>numeral k\<close>, linarith_split] for k
 
 lemma half_nonnegative_int_iff [simp]:
   \<open>k div 2 \<ge> 0 \<longleftrightarrow> k \<ge> 0\<close> for k :: int
diff -r dc758531077b -r fcd118d9242f src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Fri Aug 19 05:49:07 2022 +0000
+++ b/src/HOL/Fields.thy	Fri Aug 19 05:49:09 2022 +0000
@@ -85,7 +85,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 [arith_split] = nat_diff_split split_min split_max
+lemmas [linarith_split] = nat_diff_split split_min split_max
 
 text\<open>Lemmas \<open>divide_simps\<close> move division to the outside and eliminates them on (in)equalities.\<close>
 
diff -r dc758531077b -r fcd118d9242f src/HOL/Int.thy
--- a/src/HOL/Int.thy	Fri Aug 19 05:49:07 2022 +0000
+++ b/src/HOL/Int.thy	Fri Aug 19 05:49:09 2022 +0000
@@ -652,7 +652,7 @@
   "nat (of_bool P) = of_bool P"
   by auto
 
-lemma split_nat [arith_split]: "P (nat i) \<longleftrightarrow> ((\<forall>n. i = int n \<longrightarrow> P n) \<and> (i < 0 \<longrightarrow> P 0))"
+lemma split_nat [linarith_split]: "P (nat i) \<longleftrightarrow> ((\<forall>n. i = int n \<longrightarrow> P n) \<and> (i < 0 \<longrightarrow> P 0))"
   (is "?P = (?L \<and> ?R)")
   for i :: int
 proof (cases "i < 0")
@@ -739,11 +739,11 @@
 
 text \<open>
   This version is proved for all ordered rings, not just integers!
-  It is proved here because attribute \<open>arith_split\<close> is not available
+  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 [arith_split, no_atp]: "P \<bar>a\<bar> \<longleftrightarrow> (0 \<le> a \<longrightarrow> P a) \<and> (a < 0 \<longrightarrow> P (- a))"
+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)
 
diff -r dc758531077b -r fcd118d9242f src/HOL/Numeral_Simprocs.thy
--- a/src/HOL/Numeral_Simprocs.thy	Fri Aug 19 05:49:07 2022 +0000
+++ b/src/HOL/Numeral_Simprocs.thy	Fri Aug 19 05:49:09 2022 +0000
@@ -20,8 +20,8 @@
   numeral_One [symmetric] uminus_numeral_One [symmetric] Suc_eq_plus1
   eq_numeral_iff_iszero not_iszero_Numeral1
 
-declare split_div [of _ _ "numeral k", arith_split] for k
-declare split_mod [of _ _ "numeral k", arith_split] for k
+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>
 
diff -r dc758531077b -r fcd118d9242f src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Fri Aug 19 05:49:07 2022 +0000
+++ b/src/HOL/Tools/lin_arith.ML	Fri Aug 19 05:49:09 2022 +0000
@@ -961,7 +961,7 @@
 val global_setup =
   map_theory_simpset (fn ctxt => ctxt
     addSolver (mk_solver "lin_arith" (add_arith_facts #> Fast_Arith.prems_lin_arith_tac))) #>
-  Attrib.setup \<^binding>\<open>arith_split\<close> (Scan.succeed (Thm.declaration_attribute add_split))
+  Attrib.setup \<^binding>\<open>linarith_split\<close> (Scan.succeed (Thm.declaration_attribute add_split))
     "declaration of split rules for arithmetic procedure" #>
   Method.setup \<^binding>\<open>linarith\<close>
     (Scan.succeed (fn ctxt =>
diff -r dc758531077b -r fcd118d9242f src/HOL/ex/Arith_Examples.thy
--- a/src/HOL/ex/Arith_Examples.thy	Fri Aug 19 05:49:07 2022 +0000
+++ b/src/HOL/ex/Arith_Examples.thy	Fri Aug 19 05:49:09 2022 +0000
@@ -98,13 +98,13 @@
   by linarith
 
 lemma "(i::nat) mod 0 = i"
-  using split_mod [of _ _ 0, arith_split]
+  using split_mod [of _ _ 0, linarith_split]
     \<comment> \<open>rule \<^text>\<open>split_mod\<close> is only declared by default for numerals\<close>
   by linarith
 
 lemma "(i::nat) mod 1 = 0"
   (* rule split_mod is only declared by default for numerals *)
-  using split_mod [of _ _ 1, arith_split]
+  using split_mod [of _ _ 1, linarith_split]
     \<comment> \<open>rule \<^text>\<open>split_mod\<close> is only declared by default for numerals\<close>
   by linarith
 
@@ -112,12 +112,12 @@
   by linarith
 
 lemma "(i::int) mod 0 = i"
-  using split_zmod [of _ _ 0, arith_split]
+  using split_zmod [of _ _ 0, linarith_split]
     \<comment> \<open>rule \<^text>\<open>split_zmod\<close> is only declared by default for numerals\<close>
   by linarith
 
 lemma "(i::int) mod 1 = 0"
-  using split_zmod [of _ _ "1", arith_split]
+  using split_zmod [of _ _ "1", linarith_split]
     \<comment> \<open>rule \<^text>\<open>split_zmod\<close> is only declared by default for numerals\<close>
   by linarith