src/HOL/Divides.thy
 changeset 54489 03ff4d1e6784 parent 54230 b1d955791529 child 55085 0e8e4dc55866
```     1.1 --- a/src/HOL/Divides.thy	Tue Nov 19 01:30:14 2013 +0100
1.2 +++ b/src/HOL/Divides.thy	Tue Nov 19 10:05:53 2013 +0100
1.3 @@ -1919,10 +1919,9 @@
1.4    val zero = @{term "0 :: int"}
1.5    val less = @{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"}
1.6    val le = @{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"}
1.7 -  val simps = @{thms arith_simps} @ @{thms rel_simps} @
1.8 -    map (fn th => th RS sym) [@{thm numeral_1_eq_1}]
1.9 -  fun prove ctxt goal = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop goal)
1.10 -    (K (ALLGOALS (full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps))));
1.11 +  val simps = @{thms arith_simps} @ @{thms rel_simps} @ [@{thm numeral_1_eq_1 [symmetric]}]
1.12 +  fun prove ctxt goal = (writeln "prove"; Goal.prove ctxt [] [] (HOLogic.mk_Trueprop goal)
1.13 +    (K (ALLGOALS (full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps)))));
1.14    fun binary_proc proc ctxt ct =
1.15      (case Thm.term_of ct of
1.16        _ \$ t \$ u =>
1.17 @@ -1945,23 +1944,23 @@
1.18
1.19  simproc_setup binary_int_div
1.20    ("numeral m div numeral n :: int" |
1.21 -   "numeral m div neg_numeral n :: int" |
1.22 -   "neg_numeral m div numeral n :: int" |
1.23 -   "neg_numeral m div neg_numeral n :: int") =
1.24 +   "numeral m div - numeral n :: int" |
1.25 +   "- numeral m div numeral n :: int" |
1.26 +   "- numeral m div - numeral n :: int") =
1.27    {* K (divmod_proc @{thm int_div_pos_eq} @{thm int_div_neg_eq}) *}
1.28
1.29  simproc_setup binary_int_mod
1.30    ("numeral m mod numeral n :: int" |
1.31 -   "numeral m mod neg_numeral n :: int" |
1.32 -   "neg_numeral m mod numeral n :: int" |
1.33 -   "neg_numeral m mod neg_numeral n :: int") =
1.34 +   "numeral m mod - numeral n :: int" |
1.35 +   "- numeral m mod numeral n :: int" |
1.36 +   "- numeral m mod - numeral n :: int") =
1.37    {* K (divmod_proc @{thm int_mod_pos_eq} @{thm int_mod_neg_eq}) *}
1.38
1.39  lemmas posDivAlg_eqn_numeral [simp] =
1.40      posDivAlg_eqn [of "numeral v" "numeral w", OF zero_less_numeral] for v w
1.41
1.42  lemmas negDivAlg_eqn_numeral [simp] =
1.43 -    negDivAlg_eqn [of "numeral v" "neg_numeral w", OF zero_less_numeral] for v w
1.44 +    negDivAlg_eqn [of "numeral v" "- numeral w", OF zero_less_numeral] for v w
1.45
1.46
1.47  text{*Special-case simplification *}
1.48 @@ -1973,14 +1972,14 @@
1.49    div_pos_pos [OF zero_less_one, of "numeral w", OF zero_le_numeral] for w
1.50
1.51  lemmas div_pos_neg_1_numeral [simp] =
1.52 -  div_pos_neg [OF zero_less_one, of "neg_numeral w",
1.53 +  div_pos_neg [OF zero_less_one, of "- numeral w",
1.54    OF neg_numeral_less_zero] for w
1.55
1.56  lemmas mod_pos_pos_1_numeral [simp] =
1.57    mod_pos_pos [OF zero_less_one, of "numeral w", OF zero_le_numeral] for w
1.58
1.59  lemmas mod_pos_neg_1_numeral [simp] =
1.60 -  mod_pos_neg [OF zero_less_one, of "neg_numeral w",
1.61 +  mod_pos_neg [OF zero_less_one, of "- numeral w",
1.62    OF neg_numeral_less_zero] for w
1.63
1.64  lemmas posDivAlg_eqn_1_numeral [simp] =
1.65 @@ -2290,6 +2289,8 @@
1.66    shows "divmod_int_rel (1 + 2*a) (2*b) (q, 1 + 2*r)"
1.67    using assms unfolding divmod_int_rel_def by auto
1.68
1.69 +declaration {* K (Lin_Arith.add_simps @{thms uminus_numeral_One}) *}
1.70 +
1.71  lemma neg_divmod_int_rel_mult_2:
1.72    assumes "b \<le> 0"
1.73    assumes "divmod_int_rel (a + 1) b (q, r)"
1.74 @@ -2427,13 +2428,13 @@
1.75
1.76  lemma dvd_neg_numeral_left [simp]:
1.77    fixes y :: "'a::comm_ring_1"
1.78 -  shows "(neg_numeral k) dvd y \<longleftrightarrow> (numeral k) dvd y"
1.79 -  unfolding neg_numeral_def minus_dvd_iff ..
1.80 +  shows "(- numeral k) dvd y \<longleftrightarrow> (numeral k) dvd y"
1.81 +  by (fact minus_dvd_iff)
1.82
1.83  lemma dvd_neg_numeral_right [simp]:
1.84    fixes x :: "'a::comm_ring_1"
1.85 -  shows "x dvd (neg_numeral k) \<longleftrightarrow> x dvd (numeral k)"
1.86 -  unfolding neg_numeral_def dvd_minus_iff ..
1.87 +  shows "x dvd (- numeral k) \<longleftrightarrow> x dvd (numeral k)"
1.88 +  by (fact dvd_minus_iff)
1.89
1.90  lemmas dvd_eq_mod_eq_0_numeral [simp] =
1.91    dvd_eq_mod_eq_0 [of "numeral x" "numeral y"] for x y
```