--- 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.
--- 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.
--- 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"
--- 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
--- 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>
--- 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)
--- 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>
--- 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 =>
--- 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