# HG changeset patch
# User haftmann
# Date 1561187935 0
# Node ID 4a327c061870b0d6e0072558e3966abbcf648251
# Parent  a80ad0ac0837bb13f2b5b3edd38563fe091f0c00
streamlined setup for linear algebra, particularly removed redundant rule declarations

diff -r a80ad0ac0837 -r 4a327c061870 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Sat Jun 22 06:25:34 2019 +0000
+++ b/src/HOL/Fields.thy	Sat Jun 22 07:18:55 2019 +0000
@@ -60,26 +60,33 @@
 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 Lin_Arith.setup\<close>
+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}
+  #> Lin_Arith.add_simps @{thms simp_thms ring_distribs if_True if_False
+      minus_diff_eq
+      add_0_left add_0_right order_less_irrefl
+      zero_neq_one zero_less_one zero_le_one
+      zero_neq_one [THEN not_sym] not_one_le_zero not_one_less_zero
+      add_Suc add_Suc_right nat.inject
+      Suc_le_mono Suc_less_eq Zero_not_Suc
+      Suc_not_Zero le_0_eq One_nat_def}
+  #> Lin_Arith.add_simprocs [\<^simproc>\<open>group_cancel_add\<close>, \<^simproc>\<open>group_cancel_diff\<close>,
+      \<^simproc>\<open>group_cancel_eq\<close>, \<^simproc>\<open>group_cancel_le\<close>,
+      \<^simproc>\<open>group_cancel_less\<close>,
+      \<^simproc>\<open>nateq_cancel_sums\<close>,\<^simproc>\<open>natless_cancel_sums\<close>,
+      \<^simproc>\<open>natle_cancel_sums\<close>])\<close>
 
 simproc_setup fast_arith_nat ("(m::nat) < n" | "(m::nat) \<le> n" | "(m::nat) = n") =
-  \<open>K Lin_Arith.simproc\<close>
-(* Because of this simproc, the arithmetic solver is really only
-useful to detect inconsistencies among the premises for subgoals which are
-*not* themselves (in)equalities, because the latter activate
-fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
-solver all the time rather than add the additional check. *)
+  \<open>K Lin_Arith.simproc\<close> \<comment> \<open>Because of this simproc, the arithmetic solver is
+   really only useful to detect inconsistencies among the premises for subgoals which are
+   *not* themselves (in)equalities, because the latter activate
+   fast_nat_arith_simproc 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
 
-context linordered_nonzero_semiring
-begin
-lemma of_nat_max: "of_nat (max x y) = max (of_nat x) (of_nat y)"
-  by (auto simp: max_def)
-
-lemma of_nat_min: "of_nat (min x y) = min (of_nat x) (of_nat y)"
-  by (auto simp: min_def)
-end
 
 text\<open>Lemmas \<open>divide_simps\<close> move division to the outside and eliminates them on (in)equalities.\<close>
 
diff -r a80ad0ac0837 -r 4a327c061870 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Sat Jun 22 06:25:34 2019 +0000
+++ b/src/HOL/Int.thy	Sat Jun 22 07:18:55 2019 +0000
@@ -1086,11 +1086,27 @@
 
 subsection \<open>Setting up simplification procedures\<close>
 
-lemmas of_int_simps [no_atp] =
-  of_int_0 of_int_1 of_int_add of_int_mult
+ML_file \<open>Tools/int_arith.ML\<close>
 
-ML_file \<open>Tools/int_arith.ML\<close>
-declaration \<open>K Int_Arith.setup\<close>
+declaration \<open>K (
+  Lin_Arith.add_discrete_type \<^type_name>\<open>Int.int\<close>
+  #> Lin_Arith.add_lessD @{thm zless_imp_add1_zle}
+  #> Lin_Arith.add_inj_thms @{thms of_nat_le_iff [THEN iffD2] of_nat_eq_iff [THEN iffD2]}
+  #> Lin_Arith.add_inj_const (\<^const_name>\<open>of_nat\<close>, \<^typ>\<open>nat \<Rightarrow> int\<close>)
+  #> Lin_Arith.add_simps
+      @{thms of_int_0 of_int_1 of_int_add of_int_mult of_int_numeral of_int_neg_numeral nat_0 nat_1 diff_nat_numeral nat_numeral
+      neg_less_iff_less
+      True_implies_equals
+      distrib_left [where a = "numeral v" for v]
+      distrib_left [where a = "- numeral v" for v]
+      div_by_1 div_0
+      times_divide_eq_right times_divide_eq_left
+      minus_divide_left [THEN sym] minus_divide_right [THEN sym]
+      add_divide_distrib diff_divide_distrib
+      of_int_minus of_int_diff
+      of_int_of_nat_eq}
+  #> Lin_Arith.add_simprocs [Int_Arith.zero_one_idom_simproc]
+)\<close>
 
 simproc_setup fast_arith
   ("(m::'a::linordered_idom) < n" |
diff -r a80ad0ac0837 -r 4a327c061870 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sat Jun 22 06:25:34 2019 +0000
+++ b/src/HOL/Nat.thy	Sat Jun 22 07:18:55 2019 +0000
@@ -1773,19 +1773,32 @@
 
 end
 
+context linordered_nonzero_semiring
+begin
+
+lemma of_nat_max: "of_nat (max x y) = max (of_nat x) (of_nat y)"
+  by (auto simp: max_def ord_class.max_def)
+
+lemma of_nat_min: "of_nat (min x y) = min (of_nat x) (of_nat y)"
+  by (auto simp: min_def ord_class.min_def)
+
+end
 
 context linordered_semidom
 begin
+
 subclass linordered_nonzero_semiring ..
+
 subclass semiring_char_0 ..
+
 end
 
-
 context linordered_idom
 begin
 
-lemma abs_of_nat [simp]: "\<bar>of_nat n\<bar> = of_nat n"
-  unfolding abs_if by auto
+lemma abs_of_nat [simp]:
+  "\<bar>of_nat n\<bar> = of_nat n"
+  by (simp add: abs_if)
 
 lemma sgn_of_nat [simp]:
   "sgn (of_nat n) = of_bool (n > 0)"
diff -r a80ad0ac0837 -r 4a327c061870 src/HOL/Nonstandard_Analysis/HyperDef.thy
--- a/src/HOL/Nonstandard_Analysis/HyperDef.thy	Sat Jun 22 06:25:34 2019 +0000
+++ b/src/HOL/Nonstandard_Analysis/HyperDef.thy	Sat Jun 22 07:18:55 2019 +0000
@@ -253,11 +253,11 @@
   by (simp add: star_of_def [symmetric])
 
 declaration \<open>
-  K (Lin_Arith.add_inj_thms [@{thm star_of_le} RS iffD2,
-    @{thm star_of_less} RS iffD2, @{thm star_of_eq} RS iffD2]
-  #> Lin_Arith.add_simps [@{thm star_of_zero}, @{thm star_of_one},
-      @{thm star_of_numeral}, @{thm star_of_add},
-      @{thm star_of_minus}, @{thm star_of_diff}, @{thm star_of_mult}]
+  K (Lin_Arith.add_simps @{thms star_of_zero star_of_one
+      star_of_numeral star_of_add
+      star_of_minus star_of_diff star_of_mult}
+  #> Lin_Arith.add_inj_thms @{thms star_of_le [THEN iffD2]
+      star_of_less [THEN iffD2] star_of_eq [THEN iffD2]}
   #> Lin_Arith.add_inj_const (\<^const_name>\<open>StarDef.star_of\<close>, \<^typ>\<open>real \<Rightarrow> hypreal\<close>))
 \<close>
 
diff -r a80ad0ac0837 -r 4a327c061870 src/HOL/Num.thy
--- a/src/HOL/Num.thy	Sat Jun 22 06:25:34 2019 +0000
+++ b/src/HOL/Num.thy	Sat Jun 22 07:18:55 2019 +0000
@@ -1370,14 +1370,13 @@
     else Numeral.mk_cnumber (Thm.ctyp_of ctxt T) n;
 in
   K (
-    Lin_Arith.add_simps
-      @{thms arith_simps more_arith_simps rel_simps pred_numeral_simps
-        arith_special numeral_One of_nat_simps uminus_numeral_One}
+    Lin_Arith.set_number_of number_of
     #> Lin_Arith.add_simps
-      @{thms Suc_numeral Let_numeral Let_neg_numeral Let_0 Let_1
+      @{thms arith_simps more_arith_simps rel_simps pred_numeral_simps
+        arith_special numeral_One of_nat_simps uminus_numeral_One
+        Suc_numeral Let_numeral Let_neg_numeral Let_0 Let_1
         le_Suc_numeral le_numeral_Suc less_Suc_numeral less_numeral_Suc
-        Suc_eq_numeral eq_numeral_Suc mult_Suc mult_Suc_right of_nat_numeral}
-    #> Lin_Arith.set_number_of number_of)
+        Suc_eq_numeral eq_numeral_Suc mult_Suc mult_Suc_right of_nat_numeral})
 end
 \<close>
 
diff -r a80ad0ac0837 -r 4a327c061870 src/HOL/Numeral_Simprocs.thy
--- a/src/HOL/Numeral_Simprocs.thy	Sat Jun 22 06:25:34 2019 +0000
+++ b/src/HOL/Numeral_Simprocs.thy	Sat Jun 22 07:18:55 2019 +0000
@@ -290,13 +290,13 @@
        \<^simproc>\<open>inteq_cancel_numerals\<close>,
        \<^simproc>\<open>intless_cancel_numerals\<close>,
        \<^simproc>\<open>intle_cancel_numerals\<close>,
-       \<^simproc>\<open>field_combine_numerals\<close>]
-  #> Lin_Arith.add_simprocs
-      [\<^simproc>\<open>nat_combine_numerals\<close>,
+       \<^simproc>\<open>field_combine_numerals\<close>,
+       \<^simproc>\<open>nat_combine_numerals\<close>,
        \<^simproc>\<open>nateq_cancel_numerals\<close>,
        \<^simproc>\<open>natless_cancel_numerals\<close>,
        \<^simproc>\<open>natle_cancel_numerals\<close>,
-       \<^simproc>\<open>natdiff_cancel_numerals\<close>])
+       \<^simproc>\<open>natdiff_cancel_numerals\<close>,
+       Numeral_Simprocs.field_divide_cancel_numeral_factor])
 \<close>
 
 end
diff -r a80ad0ac0837 -r 4a327c061870 src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Sat Jun 22 06:25:34 2019 +0000
+++ b/src/HOL/Rat.thy	Sat Jun 22 07:18:55 2019 +0000
@@ -647,21 +647,8 @@
 subsection \<open>Linear arithmetic setup\<close>
 
 declaration \<open>
-  K (Lin_Arith.add_inj_thms [@{thm of_nat_le_iff} RS iffD2, @{thm of_nat_eq_iff} RS iffD2]
-    (* not needed because x < (y::nat) can be rewritten as Suc x <= y: of_nat_less_iff RS iffD2 *)
-  #> Lin_Arith.add_inj_thms [@{thm of_int_le_iff} RS iffD2, @{thm of_int_eq_iff} RS iffD2]
+  K (Lin_Arith.add_inj_thms @{thms of_int_le_iff [THEN iffD2] of_int_eq_iff [THEN iffD2]}
     (* not needed because x < (y::int) can be rewritten as x + 1 <= y: of_int_less_iff RS iffD2 *)
-  #> Lin_Arith.add_simps [@{thm neg_less_iff_less},
-      @{thm True_implies_equals},
-      @{thm distrib_left [where a = "numeral v" for v]},
-      @{thm distrib_left [where a = "- numeral v" for v]},
-      @{thm div_by_1}, @{thm div_0},
-      @{thm times_divide_eq_right}, @{thm times_divide_eq_left},
-      @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
-      @{thm add_divide_distrib}, @{thm diff_divide_distrib},
-      @{thm of_int_minus}, @{thm of_int_diff},
-      @{thm of_int_of_nat_eq}]
-  #> Lin_Arith.add_simprocs [Numeral_Simprocs.field_divide_cancel_numeral_factor]
   #> Lin_Arith.add_inj_const (\<^const_name>\<open>of_nat\<close>, \<^typ>\<open>nat \<Rightarrow> rat\<close>)
   #> Lin_Arith.add_inj_const (\<^const_name>\<open>of_int\<close>, \<^typ>\<open>int \<Rightarrow> rat\<close>))
 \<close>
diff -r a80ad0ac0837 -r 4a327c061870 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Sat Jun 22 06:25:34 2019 +0000
+++ b/src/HOL/Real.thy	Sat Jun 22 07:18:55 2019 +0000
@@ -1253,16 +1253,7 @@
 subsection \<open>Numerals and Arithmetic\<close>
 
 declaration \<open>
-  K (Lin_Arith.add_inj_thms [@{thm of_nat_le_iff} RS iffD2, @{thm of_nat_eq_iff} RS iffD2]
-    (* not needed because x < (y::nat) can be rewritten as Suc x <= y: of_nat_less_iff RS iffD2 *)
-  #> Lin_Arith.add_inj_thms [@{thm of_int_le_iff} RS iffD2, @{thm of_nat_eq_iff} RS iffD2]
-    (* not needed because x < (y::int) can be rewritten as x + 1 <= y: of_int_less_iff RS iffD2 *)
-  #> Lin_Arith.add_simps [@{thm of_nat_0}, @{thm of_nat_Suc}, @{thm of_nat_add},
-      @{thm of_nat_mult}, @{thm of_int_0}, @{thm of_int_1},
-      @{thm of_int_add}, @{thm of_int_minus}, @{thm of_int_diff},
-      @{thm of_int_mult}, @{thm of_int_of_nat_eq},
-      @{thm of_nat_numeral}, @{thm of_int_numeral}, @{thm of_int_neg_numeral}]
-  #> Lin_Arith.add_inj_const (\<^const_name>\<open>of_nat\<close>, \<^typ>\<open>nat \<Rightarrow> real\<close>)
+  K (Lin_Arith.add_inj_const (\<^const_name>\<open>of_nat\<close>, \<^typ>\<open>nat \<Rightarrow> real\<close>)
   #> Lin_Arith.add_inj_const (\<^const_name>\<open>of_int\<close>, \<^typ>\<open>int \<Rightarrow> real\<close>))
 \<close>
 
diff -r a80ad0ac0837 -r 4a327c061870 src/HOL/Tools/int_arith.ML
--- a/src/HOL/Tools/int_arith.ML	Sat Jun 22 06:25:34 2019 +0000
+++ b/src/HOL/Tools/int_arith.ML	Sat Jun 22 07:18:55 2019 +0000
@@ -1,11 +1,11 @@
 (* Author: Tobias Nipkow
 
-Instantiation of the generic linear arithmetic package for int.
+A special simproc for the instantiation of the generic linear arithmetic package for int.
 *)
 
 signature INT_ARITH =
 sig
-  val setup: Context.generic -> Context.generic
+  val zero_one_idom_simproc: simproc
 end
 
 structure Int_Arith : INT_ARITH =
@@ -25,7 +25,7 @@
 val zero_to_of_int_zero_simproc =
   Simplifier.make_simproc \<^context> "zero_to_of_int_zero_simproc"
    {lhss = [\<^term>\<open>0::'a::ring\<close>],
-    proc = fn _ => fn ctxt => fn ct =>
+    proc = fn _ => fn _ => fn ct =>
       let val T = Thm.ctyp_of_cterm ct in
         if Thm.typ_of T = \<^typ>\<open>int\<close> then NONE
         else SOME (Thm.instantiate' [SOME T] [] zeroth)
@@ -36,7 +36,7 @@
 val one_to_of_int_one_simproc =
   Simplifier.make_simproc \<^context> "one_to_of_int_one_simproc"
    {lhss = [\<^term>\<open>1::'a::ring_1\<close>],
-    proc = fn _ => fn ctxt => fn ct =>
+    proc = fn _ => fn _ => fn ct =>
       let val T = Thm.ctyp_of_cterm ct in
         if Thm.typ_of T = \<^typ>\<open>int\<close> then NONE
         else SOME (Thm.instantiate' [SOME T] [] oneth)
@@ -53,12 +53,14 @@
   | check _ = false;
 
 val conv_ss =
-  simpset_of (put_simpset HOL_basic_ss \<^context>
-    addsimps
-     ((map (fn th => th RS sym) [@{thm of_int_add}, @{thm of_int_mult},
-             @{thm of_int_diff},  @{thm of_int_minus}])@
-      [@{thm of_int_less_iff}, @{thm of_int_le_iff}, @{thm of_int_eq_iff}])
-     addsimprocs [zero_to_of_int_zero_simproc,one_to_of_int_one_simproc]);
+  \<^context>
+  |> put_simpset HOL_basic_ss
+  |> fold (Simplifier.add_simp o (fn th => th RS sym))
+       @{thms of_int_add of_int_mult
+         of_int_diff of_int_minus of_int_less_iff
+         of_int_le_iff of_int_eq_iff}
+  |> (fn ss => ss addsimprocs [zero_to_of_int_zero_simproc, one_to_of_int_one_simproc])
+  |> simpset_of;
 
 val zero_one_idom_simproc =
   Simplifier.make_simproc \<^context> "zero_one_idom_simproc"
@@ -71,21 +73,4 @@
       then SOME (Simplifier.rewrite (put_simpset conv_ss ctxt) ct)
       else NONE};
 
-
-fun number_of ctxt T n =
-  if not (Sign.of_sort (Proof_Context.theory_of ctxt) (T, \<^sort>\<open>numeral\<close>))
-  then raise CTERM ("number_of", [])
-  else Numeral.mk_cnumber (Thm.ctyp_of ctxt T) n;
-
-val setup =
-  Lin_Arith.add_inj_thms [@{thm of_nat_le_iff} RS iffD2, @{thm of_nat_eq_iff} RS iffD2]
-  #> Lin_Arith.add_lessD @{thm zless_imp_add1_zle}
-  #> Lin_Arith.add_simps @{thms of_nat_simps of_int_simps}
-  #> Lin_Arith.add_simps
-      [@{thm of_int_numeral}, @{thm nat_0}, @{thm nat_1}, @{thm diff_nat_numeral}, @{thm nat_numeral}]
-  #> Lin_Arith.add_simprocs [zero_one_idom_simproc]
-  #> Lin_Arith.set_number_of number_of
-  #> Lin_Arith.add_inj_const (\<^const_name>\<open>of_nat\<close>, HOLogic.natT --> HOLogic.intT)
-  #> Lin_Arith.add_discrete_type \<^type_name>\<open>Int.int\<close>
-
 end;
diff -r a80ad0ac0837 -r 4a327c061870 src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Sat Jun 22 06:25:34 2019 +0000
+++ b/src/HOL/Tools/lin_arith.ML	Sat Jun 22 07:18:55 2019 +0000
@@ -17,8 +17,8 @@
   val add_inj_const: string * typ -> Context.generic -> Context.generic
   val add_discrete_type: string -> Context.generic -> Context.generic
   val set_number_of: (Proof.context -> typ -> int -> cterm) -> Context.generic -> Context.generic
-  val setup: Context.generic -> Context.generic
   val global_setup: theory -> theory
+  val init_arith_data: Context.generic -> Context.generic
   val split_limit: int Config.T
   val neq_limit: int Config.T
   val trace: bool Config.T
@@ -973,23 +973,4 @@
           THEN' tac ctxt)))) "linear arithmetic" #>
   Arith_Data.add_tactic "linear arithmetic" tac;
 
-val setup =
-  init_arith_data
-  #> add_discrete_type \<^type_name>\<open>nat\<close>
-  #> add_lessD @{thm Suc_leI}
-  #> add_simps (@{thms simp_thms} @ @{thms ring_distribs} @ [@{thm if_True}, @{thm if_False},
-      @{thm minus_diff_eq},
-      @{thm add_0_left}, @{thm add_0_right}, @{thm order_less_irrefl},
-      @{thm zero_neq_one}, @{thm zero_less_one}, @{thm zero_le_one},
-      @{thm zero_neq_one} RS not_sym, @{thm not_one_le_zero}, @{thm not_one_less_zero}])
-  #> add_simps [@{thm add_Suc}, @{thm add_Suc_right}, @{thm nat.inject},
-      @{thm Suc_le_mono}, @{thm Suc_less_eq}, @{thm Zero_not_Suc},
-      @{thm Suc_not_Zero}, @{thm le_0_eq}, @{thm One_nat_def}]
-  #> add_simprocs [\<^simproc>\<open>group_cancel_add\<close>, \<^simproc>\<open>group_cancel_diff\<close>,
-      \<^simproc>\<open>group_cancel_eq\<close>, \<^simproc>\<open>group_cancel_le\<close>,
-      \<^simproc>\<open>group_cancel_less\<close>]
-     (*abel_cancel helps it work in abstract algebraic domains*)
-  #> add_simprocs [\<^simproc>\<open>nateq_cancel_sums\<close>,\<^simproc>\<open>natless_cancel_sums\<close>,
-      \<^simproc>\<open>natle_cancel_sums\<close>];
-
 end;
diff -r a80ad0ac0837 -r 4a327c061870 src/HOL/ex/Arith_Examples.thy
--- a/src/HOL/ex/Arith_Examples.thy	Sat Jun 22 06:25:34 2019 +0000
+++ b/src/HOL/ex/Arith_Examples.thy	Sat Jun 22 07:18:55 2019 +0000
@@ -98,26 +98,27 @@
   by linarith
 
 lemma "(i::nat) mod 0 = i"
-  (* rule split_mod is only declared by default for numerals *)
-  using split_mod [of _ _ "0", arith_split]
+  using split_mod [of _ _ 0, arith_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, arith_split]
+    \<comment> \<open>rule \<^text>\<open>split_mod\<close> is only declared by default for numerals\<close>
   by linarith
 
 lemma "(i::nat) mod 42 <= 41"
   by linarith
 
 lemma "(i::int) mod 0 = i"
-  (* rule split_zmod is only declared by default for numerals *)
-  using split_zmod [of _ _ "0", arith_split]
+  using split_zmod [of _ _ 0, arith_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"
-  (* rule split_zmod is only declared by default for numerals *)
   using split_zmod [of _ _ "1", arith_split]
+    \<comment> \<open>rule \<^text>\<open>split_zmod\<close> is only declared by default for numerals\<close>
   by linarith
 
 lemma "(i::int) mod 42 <= 41"