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