streamlined setup for linear algebra, particularly removed redundant rule declarations
authorhaftmann
Sat Jun 22 07:18:55 2019 +0000 (4 weeks ago)
changeset 703564a327c061870
parent 70355 a80ad0ac0837
child 70357 4d0b789e4e21
streamlined setup for linear algebra, particularly removed redundant rule declarations
src/HOL/Fields.thy
src/HOL/Int.thy
src/HOL/Nat.thy
src/HOL/Nonstandard_Analysis/HyperDef.thy
src/HOL/Num.thy
src/HOL/Numeral_Simprocs.thy
src/HOL/Rat.thy
src/HOL/Real.thy
src/HOL/Tools/int_arith.ML
src/HOL/Tools/lin_arith.ML
src/HOL/ex/Arith_Examples.thy
     1.1 --- a/src/HOL/Fields.thy	Sat Jun 22 06:25:34 2019 +0000
     1.2 +++ b/src/HOL/Fields.thy	Sat Jun 22 07:18:55 2019 +0000
     1.3 @@ -60,26 +60,33 @@
     1.4  ML_file \<open>~~/src/Provers/Arith/fast_lin_arith.ML\<close>
     1.5  ML_file \<open>Tools/lin_arith.ML\<close>
     1.6  setup \<open>Lin_Arith.global_setup\<close>
     1.7 -declaration \<open>K Lin_Arith.setup\<close>
     1.8 +declaration \<open>K (
     1.9 +  Lin_Arith.init_arith_data
    1.10 +  #> Lin_Arith.add_discrete_type \<^type_name>\<open>nat\<close>
    1.11 +  #> Lin_Arith.add_lessD @{thm Suc_leI}
    1.12 +  #> Lin_Arith.add_simps @{thms simp_thms ring_distribs if_True if_False
    1.13 +      minus_diff_eq
    1.14 +      add_0_left add_0_right order_less_irrefl
    1.15 +      zero_neq_one zero_less_one zero_le_one
    1.16 +      zero_neq_one [THEN not_sym] not_one_le_zero not_one_less_zero
    1.17 +      add_Suc add_Suc_right nat.inject
    1.18 +      Suc_le_mono Suc_less_eq Zero_not_Suc
    1.19 +      Suc_not_Zero le_0_eq One_nat_def}
    1.20 +  #> Lin_Arith.add_simprocs [\<^simproc>\<open>group_cancel_add\<close>, \<^simproc>\<open>group_cancel_diff\<close>,
    1.21 +      \<^simproc>\<open>group_cancel_eq\<close>, \<^simproc>\<open>group_cancel_le\<close>,
    1.22 +      \<^simproc>\<open>group_cancel_less\<close>,
    1.23 +      \<^simproc>\<open>nateq_cancel_sums\<close>,\<^simproc>\<open>natless_cancel_sums\<close>,
    1.24 +      \<^simproc>\<open>natle_cancel_sums\<close>])\<close>
    1.25  
    1.26  simproc_setup fast_arith_nat ("(m::nat) < n" | "(m::nat) \<le> n" | "(m::nat) = n") =
    1.27 -  \<open>K Lin_Arith.simproc\<close>
    1.28 -(* Because of this simproc, the arithmetic solver is really only
    1.29 -useful to detect inconsistencies among the premises for subgoals which are
    1.30 -*not* themselves (in)equalities, because the latter activate
    1.31 -fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
    1.32 -solver all the time rather than add the additional check. *)
    1.33 +  \<open>K Lin_Arith.simproc\<close> \<comment> \<open>Because of this simproc, the arithmetic solver is
    1.34 +   really only useful to detect inconsistencies among the premises for subgoals which are
    1.35 +   *not* themselves (in)equalities, because the latter activate
    1.36 +   fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
    1.37 +   solver all the time rather than add the additional check.\<close>
    1.38  
    1.39  lemmas [arith_split] = nat_diff_split split_min split_max
    1.40  
    1.41 -context linordered_nonzero_semiring
    1.42 -begin
    1.43 -lemma of_nat_max: "of_nat (max x y) = max (of_nat x) (of_nat y)"
    1.44 -  by (auto simp: max_def)
    1.45 -
    1.46 -lemma of_nat_min: "of_nat (min x y) = min (of_nat x) (of_nat y)"
    1.47 -  by (auto simp: min_def)
    1.48 -end
    1.49  
    1.50  text\<open>Lemmas \<open>divide_simps\<close> move division to the outside and eliminates them on (in)equalities.\<close>
    1.51  
     2.1 --- a/src/HOL/Int.thy	Sat Jun 22 06:25:34 2019 +0000
     2.2 +++ b/src/HOL/Int.thy	Sat Jun 22 07:18:55 2019 +0000
     2.3 @@ -1086,11 +1086,27 @@
     2.4  
     2.5  subsection \<open>Setting up simplification procedures\<close>
     2.6  
     2.7 -lemmas of_int_simps [no_atp] =
     2.8 -  of_int_0 of_int_1 of_int_add of_int_mult
     2.9 +ML_file \<open>Tools/int_arith.ML\<close>
    2.10  
    2.11 -ML_file \<open>Tools/int_arith.ML\<close>
    2.12 -declaration \<open>K Int_Arith.setup\<close>
    2.13 +declaration \<open>K (
    2.14 +  Lin_Arith.add_discrete_type \<^type_name>\<open>Int.int\<close>
    2.15 +  #> Lin_Arith.add_lessD @{thm zless_imp_add1_zle}
    2.16 +  #> Lin_Arith.add_inj_thms @{thms of_nat_le_iff [THEN iffD2] of_nat_eq_iff [THEN iffD2]}
    2.17 +  #> Lin_Arith.add_inj_const (\<^const_name>\<open>of_nat\<close>, \<^typ>\<open>nat \<Rightarrow> int\<close>)
    2.18 +  #> Lin_Arith.add_simps
    2.19 +      @{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
    2.20 +      neg_less_iff_less
    2.21 +      True_implies_equals
    2.22 +      distrib_left [where a = "numeral v" for v]
    2.23 +      distrib_left [where a = "- numeral v" for v]
    2.24 +      div_by_1 div_0
    2.25 +      times_divide_eq_right times_divide_eq_left
    2.26 +      minus_divide_left [THEN sym] minus_divide_right [THEN sym]
    2.27 +      add_divide_distrib diff_divide_distrib
    2.28 +      of_int_minus of_int_diff
    2.29 +      of_int_of_nat_eq}
    2.30 +  #> Lin_Arith.add_simprocs [Int_Arith.zero_one_idom_simproc]
    2.31 +)\<close>
    2.32  
    2.33  simproc_setup fast_arith
    2.34    ("(m::'a::linordered_idom) < n" |
     3.1 --- a/src/HOL/Nat.thy	Sat Jun 22 06:25:34 2019 +0000
     3.2 +++ b/src/HOL/Nat.thy	Sat Jun 22 07:18:55 2019 +0000
     3.3 @@ -1773,19 +1773,32 @@
     3.4  
     3.5  end
     3.6  
     3.7 +context linordered_nonzero_semiring
     3.8 +begin
     3.9 +
    3.10 +lemma of_nat_max: "of_nat (max x y) = max (of_nat x) (of_nat y)"
    3.11 +  by (auto simp: max_def ord_class.max_def)
    3.12 +
    3.13 +lemma of_nat_min: "of_nat (min x y) = min (of_nat x) (of_nat y)"
    3.14 +  by (auto simp: min_def ord_class.min_def)
    3.15 +
    3.16 +end
    3.17  
    3.18  context linordered_semidom
    3.19  begin
    3.20 +
    3.21  subclass linordered_nonzero_semiring ..
    3.22 +
    3.23  subclass semiring_char_0 ..
    3.24 +
    3.25  end
    3.26  
    3.27 -
    3.28  context linordered_idom
    3.29  begin
    3.30  
    3.31 -lemma abs_of_nat [simp]: "\<bar>of_nat n\<bar> = of_nat n"
    3.32 -  unfolding abs_if by auto
    3.33 +lemma abs_of_nat [simp]:
    3.34 +  "\<bar>of_nat n\<bar> = of_nat n"
    3.35 +  by (simp add: abs_if)
    3.36  
    3.37  lemma sgn_of_nat [simp]:
    3.38    "sgn (of_nat n) = of_bool (n > 0)"
     4.1 --- a/src/HOL/Nonstandard_Analysis/HyperDef.thy	Sat Jun 22 06:25:34 2019 +0000
     4.2 +++ b/src/HOL/Nonstandard_Analysis/HyperDef.thy	Sat Jun 22 07:18:55 2019 +0000
     4.3 @@ -253,11 +253,11 @@
     4.4    by (simp add: star_of_def [symmetric])
     4.5  
     4.6  declaration \<open>
     4.7 -  K (Lin_Arith.add_inj_thms [@{thm star_of_le} RS iffD2,
     4.8 -    @{thm star_of_less} RS iffD2, @{thm star_of_eq} RS iffD2]
     4.9 -  #> Lin_Arith.add_simps [@{thm star_of_zero}, @{thm star_of_one},
    4.10 -      @{thm star_of_numeral}, @{thm star_of_add},
    4.11 -      @{thm star_of_minus}, @{thm star_of_diff}, @{thm star_of_mult}]
    4.12 +  K (Lin_Arith.add_simps @{thms star_of_zero star_of_one
    4.13 +      star_of_numeral star_of_add
    4.14 +      star_of_minus star_of_diff star_of_mult}
    4.15 +  #> Lin_Arith.add_inj_thms @{thms star_of_le [THEN iffD2]
    4.16 +      star_of_less [THEN iffD2] star_of_eq [THEN iffD2]}
    4.17    #> Lin_Arith.add_inj_const (\<^const_name>\<open>StarDef.star_of\<close>, \<^typ>\<open>real \<Rightarrow> hypreal\<close>))
    4.18  \<close>
    4.19  
     5.1 --- a/src/HOL/Num.thy	Sat Jun 22 06:25:34 2019 +0000
     5.2 +++ b/src/HOL/Num.thy	Sat Jun 22 07:18:55 2019 +0000
     5.3 @@ -1370,14 +1370,13 @@
     5.4      else Numeral.mk_cnumber (Thm.ctyp_of ctxt T) n;
     5.5  in
     5.6    K (
     5.7 -    Lin_Arith.add_simps
     5.8 -      @{thms arith_simps more_arith_simps rel_simps pred_numeral_simps
     5.9 -        arith_special numeral_One of_nat_simps uminus_numeral_One}
    5.10 +    Lin_Arith.set_number_of number_of
    5.11      #> Lin_Arith.add_simps
    5.12 -      @{thms Suc_numeral Let_numeral Let_neg_numeral Let_0 Let_1
    5.13 +      @{thms arith_simps more_arith_simps rel_simps pred_numeral_simps
    5.14 +        arith_special numeral_One of_nat_simps uminus_numeral_One
    5.15 +        Suc_numeral Let_numeral Let_neg_numeral Let_0 Let_1
    5.16          le_Suc_numeral le_numeral_Suc less_Suc_numeral less_numeral_Suc
    5.17 -        Suc_eq_numeral eq_numeral_Suc mult_Suc mult_Suc_right of_nat_numeral}
    5.18 -    #> Lin_Arith.set_number_of number_of)
    5.19 +        Suc_eq_numeral eq_numeral_Suc mult_Suc mult_Suc_right of_nat_numeral})
    5.20  end
    5.21  \<close>
    5.22  
     6.1 --- a/src/HOL/Numeral_Simprocs.thy	Sat Jun 22 06:25:34 2019 +0000
     6.2 +++ b/src/HOL/Numeral_Simprocs.thy	Sat Jun 22 07:18:55 2019 +0000
     6.3 @@ -290,13 +290,13 @@
     6.4         \<^simproc>\<open>inteq_cancel_numerals\<close>,
     6.5         \<^simproc>\<open>intless_cancel_numerals\<close>,
     6.6         \<^simproc>\<open>intle_cancel_numerals\<close>,
     6.7 -       \<^simproc>\<open>field_combine_numerals\<close>]
     6.8 -  #> Lin_Arith.add_simprocs
     6.9 -      [\<^simproc>\<open>nat_combine_numerals\<close>,
    6.10 +       \<^simproc>\<open>field_combine_numerals\<close>,
    6.11 +       \<^simproc>\<open>nat_combine_numerals\<close>,
    6.12         \<^simproc>\<open>nateq_cancel_numerals\<close>,
    6.13         \<^simproc>\<open>natless_cancel_numerals\<close>,
    6.14         \<^simproc>\<open>natle_cancel_numerals\<close>,
    6.15 -       \<^simproc>\<open>natdiff_cancel_numerals\<close>])
    6.16 +       \<^simproc>\<open>natdiff_cancel_numerals\<close>,
    6.17 +       Numeral_Simprocs.field_divide_cancel_numeral_factor])
    6.18  \<close>
    6.19  
    6.20  end
     7.1 --- a/src/HOL/Rat.thy	Sat Jun 22 06:25:34 2019 +0000
     7.2 +++ b/src/HOL/Rat.thy	Sat Jun 22 07:18:55 2019 +0000
     7.3 @@ -647,21 +647,8 @@
     7.4  subsection \<open>Linear arithmetic setup\<close>
     7.5  
     7.6  declaration \<open>
     7.7 -  K (Lin_Arith.add_inj_thms [@{thm of_nat_le_iff} RS iffD2, @{thm of_nat_eq_iff} RS iffD2]
     7.8 -    (* not needed because x < (y::nat) can be rewritten as Suc x <= y: of_nat_less_iff RS iffD2 *)
     7.9 -  #> Lin_Arith.add_inj_thms [@{thm of_int_le_iff} RS iffD2, @{thm of_int_eq_iff} RS iffD2]
    7.10 +  K (Lin_Arith.add_inj_thms @{thms of_int_le_iff [THEN iffD2] of_int_eq_iff [THEN iffD2]}
    7.11      (* not needed because x < (y::int) can be rewritten as x + 1 <= y: of_int_less_iff RS iffD2 *)
    7.12 -  #> Lin_Arith.add_simps [@{thm neg_less_iff_less},
    7.13 -      @{thm True_implies_equals},
    7.14 -      @{thm distrib_left [where a = "numeral v" for v]},
    7.15 -      @{thm distrib_left [where a = "- numeral v" for v]},
    7.16 -      @{thm div_by_1}, @{thm div_0},
    7.17 -      @{thm times_divide_eq_right}, @{thm times_divide_eq_left},
    7.18 -      @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
    7.19 -      @{thm add_divide_distrib}, @{thm diff_divide_distrib},
    7.20 -      @{thm of_int_minus}, @{thm of_int_diff},
    7.21 -      @{thm of_int_of_nat_eq}]
    7.22 -  #> Lin_Arith.add_simprocs [Numeral_Simprocs.field_divide_cancel_numeral_factor]
    7.23    #> Lin_Arith.add_inj_const (\<^const_name>\<open>of_nat\<close>, \<^typ>\<open>nat \<Rightarrow> rat\<close>)
    7.24    #> Lin_Arith.add_inj_const (\<^const_name>\<open>of_int\<close>, \<^typ>\<open>int \<Rightarrow> rat\<close>))
    7.25  \<close>
     8.1 --- a/src/HOL/Real.thy	Sat Jun 22 06:25:34 2019 +0000
     8.2 +++ b/src/HOL/Real.thy	Sat Jun 22 07:18:55 2019 +0000
     8.3 @@ -1253,16 +1253,7 @@
     8.4  subsection \<open>Numerals and Arithmetic\<close>
     8.5  
     8.6  declaration \<open>
     8.7 -  K (Lin_Arith.add_inj_thms [@{thm of_nat_le_iff} RS iffD2, @{thm of_nat_eq_iff} RS iffD2]
     8.8 -    (* not needed because x < (y::nat) can be rewritten as Suc x <= y: of_nat_less_iff RS iffD2 *)
     8.9 -  #> Lin_Arith.add_inj_thms [@{thm of_int_le_iff} RS iffD2, @{thm of_nat_eq_iff} RS iffD2]
    8.10 -    (* not needed because x < (y::int) can be rewritten as x + 1 <= y: of_int_less_iff RS iffD2 *)
    8.11 -  #> Lin_Arith.add_simps [@{thm of_nat_0}, @{thm of_nat_Suc}, @{thm of_nat_add},
    8.12 -      @{thm of_nat_mult}, @{thm of_int_0}, @{thm of_int_1},
    8.13 -      @{thm of_int_add}, @{thm of_int_minus}, @{thm of_int_diff},
    8.14 -      @{thm of_int_mult}, @{thm of_int_of_nat_eq},
    8.15 -      @{thm of_nat_numeral}, @{thm of_int_numeral}, @{thm of_int_neg_numeral}]
    8.16 -  #> Lin_Arith.add_inj_const (\<^const_name>\<open>of_nat\<close>, \<^typ>\<open>nat \<Rightarrow> real\<close>)
    8.17 +  K (Lin_Arith.add_inj_const (\<^const_name>\<open>of_nat\<close>, \<^typ>\<open>nat \<Rightarrow> real\<close>)
    8.18    #> Lin_Arith.add_inj_const (\<^const_name>\<open>of_int\<close>, \<^typ>\<open>int \<Rightarrow> real\<close>))
    8.19  \<close>
    8.20  
     9.1 --- a/src/HOL/Tools/int_arith.ML	Sat Jun 22 06:25:34 2019 +0000
     9.2 +++ b/src/HOL/Tools/int_arith.ML	Sat Jun 22 07:18:55 2019 +0000
     9.3 @@ -1,11 +1,11 @@
     9.4  (* Author: Tobias Nipkow
     9.5  
     9.6 -Instantiation of the generic linear arithmetic package for int.
     9.7 +A special simproc for the instantiation of the generic linear arithmetic package for int.
     9.8  *)
     9.9  
    9.10  signature INT_ARITH =
    9.11  sig
    9.12 -  val setup: Context.generic -> Context.generic
    9.13 +  val zero_one_idom_simproc: simproc
    9.14  end
    9.15  
    9.16  structure Int_Arith : INT_ARITH =
    9.17 @@ -25,7 +25,7 @@
    9.18  val zero_to_of_int_zero_simproc =
    9.19    Simplifier.make_simproc \<^context> "zero_to_of_int_zero_simproc"
    9.20     {lhss = [\<^term>\<open>0::'a::ring\<close>],
    9.21 -    proc = fn _ => fn ctxt => fn ct =>
    9.22 +    proc = fn _ => fn _ => fn ct =>
    9.23        let val T = Thm.ctyp_of_cterm ct in
    9.24          if Thm.typ_of T = \<^typ>\<open>int\<close> then NONE
    9.25          else SOME (Thm.instantiate' [SOME T] [] zeroth)
    9.26 @@ -36,7 +36,7 @@
    9.27  val one_to_of_int_one_simproc =
    9.28    Simplifier.make_simproc \<^context> "one_to_of_int_one_simproc"
    9.29     {lhss = [\<^term>\<open>1::'a::ring_1\<close>],
    9.30 -    proc = fn _ => fn ctxt => fn ct =>
    9.31 +    proc = fn _ => fn _ => fn ct =>
    9.32        let val T = Thm.ctyp_of_cterm ct in
    9.33          if Thm.typ_of T = \<^typ>\<open>int\<close> then NONE
    9.34          else SOME (Thm.instantiate' [SOME T] [] oneth)
    9.35 @@ -53,12 +53,14 @@
    9.36    | check _ = false;
    9.37  
    9.38  val conv_ss =
    9.39 -  simpset_of (put_simpset HOL_basic_ss \<^context>
    9.40 -    addsimps
    9.41 -     ((map (fn th => th RS sym) [@{thm of_int_add}, @{thm of_int_mult},
    9.42 -             @{thm of_int_diff},  @{thm of_int_minus}])@
    9.43 -      [@{thm of_int_less_iff}, @{thm of_int_le_iff}, @{thm of_int_eq_iff}])
    9.44 -     addsimprocs [zero_to_of_int_zero_simproc,one_to_of_int_one_simproc]);
    9.45 +  \<^context>
    9.46 +  |> put_simpset HOL_basic_ss
    9.47 +  |> fold (Simplifier.add_simp o (fn th => th RS sym))
    9.48 +       @{thms of_int_add of_int_mult
    9.49 +         of_int_diff of_int_minus of_int_less_iff
    9.50 +         of_int_le_iff of_int_eq_iff}
    9.51 +  |> (fn ss => ss addsimprocs [zero_to_of_int_zero_simproc, one_to_of_int_one_simproc])
    9.52 +  |> simpset_of;
    9.53  
    9.54  val zero_one_idom_simproc =
    9.55    Simplifier.make_simproc \<^context> "zero_one_idom_simproc"
    9.56 @@ -71,21 +73,4 @@
    9.57        then SOME (Simplifier.rewrite (put_simpset conv_ss ctxt) ct)
    9.58        else NONE};
    9.59  
    9.60 -
    9.61 -fun number_of ctxt T n =
    9.62 -  if not (Sign.of_sort (Proof_Context.theory_of ctxt) (T, \<^sort>\<open>numeral\<close>))
    9.63 -  then raise CTERM ("number_of", [])
    9.64 -  else Numeral.mk_cnumber (Thm.ctyp_of ctxt T) n;
    9.65 -
    9.66 -val setup =
    9.67 -  Lin_Arith.add_inj_thms [@{thm of_nat_le_iff} RS iffD2, @{thm of_nat_eq_iff} RS iffD2]
    9.68 -  #> Lin_Arith.add_lessD @{thm zless_imp_add1_zle}
    9.69 -  #> Lin_Arith.add_simps @{thms of_nat_simps of_int_simps}
    9.70 -  #> Lin_Arith.add_simps
    9.71 -      [@{thm of_int_numeral}, @{thm nat_0}, @{thm nat_1}, @{thm diff_nat_numeral}, @{thm nat_numeral}]
    9.72 -  #> Lin_Arith.add_simprocs [zero_one_idom_simproc]
    9.73 -  #> Lin_Arith.set_number_of number_of
    9.74 -  #> Lin_Arith.add_inj_const (\<^const_name>\<open>of_nat\<close>, HOLogic.natT --> HOLogic.intT)
    9.75 -  #> Lin_Arith.add_discrete_type \<^type_name>\<open>Int.int\<close>
    9.76 -
    9.77  end;
    10.1 --- a/src/HOL/Tools/lin_arith.ML	Sat Jun 22 06:25:34 2019 +0000
    10.2 +++ b/src/HOL/Tools/lin_arith.ML	Sat Jun 22 07:18:55 2019 +0000
    10.3 @@ -17,8 +17,8 @@
    10.4    val add_inj_const: string * typ -> Context.generic -> Context.generic
    10.5    val add_discrete_type: string -> Context.generic -> Context.generic
    10.6    val set_number_of: (Proof.context -> typ -> int -> cterm) -> Context.generic -> Context.generic
    10.7 -  val setup: Context.generic -> Context.generic
    10.8    val global_setup: theory -> theory
    10.9 +  val init_arith_data: Context.generic -> Context.generic
   10.10    val split_limit: int Config.T
   10.11    val neq_limit: int Config.T
   10.12    val trace: bool Config.T
   10.13 @@ -973,23 +973,4 @@
   10.14            THEN' tac ctxt)))) "linear arithmetic" #>
   10.15    Arith_Data.add_tactic "linear arithmetic" tac;
   10.16  
   10.17 -val setup =
   10.18 -  init_arith_data
   10.19 -  #> add_discrete_type \<^type_name>\<open>nat\<close>
   10.20 -  #> add_lessD @{thm Suc_leI}
   10.21 -  #> add_simps (@{thms simp_thms} @ @{thms ring_distribs} @ [@{thm if_True}, @{thm if_False},
   10.22 -      @{thm minus_diff_eq},
   10.23 -      @{thm add_0_left}, @{thm add_0_right}, @{thm order_less_irrefl},
   10.24 -      @{thm zero_neq_one}, @{thm zero_less_one}, @{thm zero_le_one},
   10.25 -      @{thm zero_neq_one} RS not_sym, @{thm not_one_le_zero}, @{thm not_one_less_zero}])
   10.26 -  #> add_simps [@{thm add_Suc}, @{thm add_Suc_right}, @{thm nat.inject},
   10.27 -      @{thm Suc_le_mono}, @{thm Suc_less_eq}, @{thm Zero_not_Suc},
   10.28 -      @{thm Suc_not_Zero}, @{thm le_0_eq}, @{thm One_nat_def}]
   10.29 -  #> add_simprocs [\<^simproc>\<open>group_cancel_add\<close>, \<^simproc>\<open>group_cancel_diff\<close>,
   10.30 -      \<^simproc>\<open>group_cancel_eq\<close>, \<^simproc>\<open>group_cancel_le\<close>,
   10.31 -      \<^simproc>\<open>group_cancel_less\<close>]
   10.32 -     (*abel_cancel helps it work in abstract algebraic domains*)
   10.33 -  #> add_simprocs [\<^simproc>\<open>nateq_cancel_sums\<close>,\<^simproc>\<open>natless_cancel_sums\<close>,
   10.34 -      \<^simproc>\<open>natle_cancel_sums\<close>];
   10.35 -
   10.36  end;
    11.1 --- a/src/HOL/ex/Arith_Examples.thy	Sat Jun 22 06:25:34 2019 +0000
    11.2 +++ b/src/HOL/ex/Arith_Examples.thy	Sat Jun 22 07:18:55 2019 +0000
    11.3 @@ -98,26 +98,27 @@
    11.4    by linarith
    11.5  
    11.6  lemma "(i::nat) mod 0 = i"
    11.7 -  (* rule split_mod is only declared by default for numerals *)
    11.8 -  using split_mod [of _ _ "0", arith_split]
    11.9 +  using split_mod [of _ _ 0, arith_split]
   11.10 +    \<comment> \<open>rule \<^text>\<open>split_mod\<close> is only declared by default for numerals\<close>
   11.11    by linarith
   11.12  
   11.13  lemma "(i::nat) mod 1 = 0"
   11.14    (* rule split_mod is only declared by default for numerals *)
   11.15 -  using split_mod [of _ _ "1", arith_split]
   11.16 +  using split_mod [of _ _ 1, arith_split]
   11.17 +    \<comment> \<open>rule \<^text>\<open>split_mod\<close> is only declared by default for numerals\<close>
   11.18    by linarith
   11.19  
   11.20  lemma "(i::nat) mod 42 <= 41"
   11.21    by linarith
   11.22  
   11.23  lemma "(i::int) mod 0 = i"
   11.24 -  (* rule split_zmod is only declared by default for numerals *)
   11.25 -  using split_zmod [of _ _ "0", arith_split]
   11.26 +  using split_zmod [of _ _ 0, arith_split]
   11.27 +    \<comment> \<open>rule \<^text>\<open>split_zmod\<close> is only declared by default for numerals\<close>
   11.28    by linarith
   11.29  
   11.30  lemma "(i::int) mod 1 = 0"
   11.31 -  (* rule split_zmod is only declared by default for numerals *)
   11.32    using split_zmod [of _ _ "1", arith_split]
   11.33 +    \<comment> \<open>rule \<^text>\<open>split_zmod\<close> is only declared by default for numerals\<close>
   11.34    by linarith
   11.35  
   11.36  lemma "(i::int) mod 42 <= 41"