src/HOL/Divides.thy
changeset 45530 0c4853bb77bf
parent 45231 d85a2fdc586c
child 45607 16b4f5774621
     1.1 --- a/src/HOL/Divides.thy	Wed Nov 16 13:58:31 2011 +0100
     1.2 +++ b/src/HOL/Divides.thy	Wed Nov 16 15:20:27 2011 +0100
     1.3 @@ -1663,13 +1663,22 @@
     1.4  
     1.5  text {*Simplify expresions in which div and mod combine numerical constants*}
     1.6  
     1.7 -lemma divmod_int_relI:
     1.8 -  "\<lbrakk>a == b * q + r; if 0 < b then 0 \<le> r \<and> r < b else b < r \<and> r \<le> 0\<rbrakk>
     1.9 -    \<Longrightarrow> divmod_int_rel a b (q, r)"
    1.10 -  unfolding divmod_int_rel_def by simp
    1.11 -
    1.12 -lemmas divmod_int_rel_div_eq = divmod_int_relI [THEN divmod_int_rel_div, THEN eq_reflection]
    1.13 -lemmas divmod_int_rel_mod_eq = divmod_int_relI [THEN divmod_int_rel_mod, THEN eq_reflection]
    1.14 +lemma int_div_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a div b = q"
    1.15 +  by (rule divmod_int_rel_div [of a b q r],
    1.16 +    simp add: divmod_int_rel_def, simp)
    1.17 +
    1.18 +lemma int_div_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a div b = q"
    1.19 +  by (rule divmod_int_rel_div [of a b q r],
    1.20 +    simp add: divmod_int_rel_def, simp)
    1.21 +
    1.22 +lemma int_mod_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a mod b = r"
    1.23 +  by (rule divmod_int_rel_mod [of a b q r],
    1.24 +    simp add: divmod_int_rel_def, simp)
    1.25 +
    1.26 +lemma int_mod_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a mod b = r"
    1.27 +  by (rule divmod_int_rel_mod [of a b q r],
    1.28 +    simp add: divmod_int_rel_def, simp)
    1.29 +
    1.30  lemmas arithmetic_simps =
    1.31    arith_simps
    1.32    add_special
    1.33 @@ -1683,12 +1692,16 @@
    1.34  (* simprocs adapted from HOL/ex/Binary.thy *)
    1.35  ML {*
    1.36  local
    1.37 -  val mk_number = HOLogic.mk_number HOLogic.intT;
    1.38 -  fun mk_cert u k l = @{term "plus :: int \<Rightarrow> int \<Rightarrow> int"} $
    1.39 -    (@{term "times :: int \<Rightarrow> int \<Rightarrow> int"} $ u $ mk_number k) $
    1.40 -      mk_number l;
    1.41 -  fun prove ctxt prop = Goal.prove ctxt [] [] prop
    1.42 -    (K (ALLGOALS (full_simp_tac (HOL_basic_ss addsimps @{thms arithmetic_simps}))));
    1.43 +  val mk_number = HOLogic.mk_number HOLogic.intT
    1.44 +  val plus = @{term "plus :: int \<Rightarrow> int \<Rightarrow> int"}
    1.45 +  val times = @{term "times :: int \<Rightarrow> int \<Rightarrow> int"}
    1.46 +  val zero = @{term "0 :: int"}
    1.47 +  val less = @{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"}
    1.48 +  val le = @{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"}
    1.49 +  val simps = @{thms arith_simps} @ @{thms rel_simps} @
    1.50 +    map (fn th => th RS sym) [@{thm numeral_0_eq_0}, @{thm numeral_1_eq_1}]
    1.51 +  fun prove ctxt goal = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop goal)
    1.52 +    (K (ALLGOALS (full_simp_tac (HOL_basic_ss addsimps simps))));
    1.53    fun binary_proc proc ss ct =
    1.54      (case Thm.term_of ct of
    1.55        _ $ t $ u =>
    1.56 @@ -1697,18 +1710,23 @@
    1.57        | NONE => NONE)
    1.58      | _ => NONE);
    1.59  in
    1.60 -  fun divmod_proc rule = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
    1.61 -    if n = 0 then NONE
    1.62 -    else let val (k, l) = Integer.div_mod m n;
    1.63 -    in SOME (rule OF [prove ctxt (Logic.mk_equals (t, mk_cert u k l))]) end);
    1.64 +  fun divmod_proc posrule negrule =
    1.65 +    binary_proc (fn ctxt => fn ((a, t), (b, u)) =>
    1.66 +      if b = 0 then NONE else let
    1.67 +        val (q, r) = pairself mk_number (Integer.div_mod a b)
    1.68 +        val goal1 = HOLogic.mk_eq (t, plus $ (times $ u $ q) $ r)
    1.69 +        val (goal2, goal3, rule) = if b > 0
    1.70 +          then (le $ zero $ r, less $ r $ u, posrule RS eq_reflection)
    1.71 +          else (le $ r $ zero, less $ u $ r, negrule RS eq_reflection)
    1.72 +      in SOME (rule OF map (prove ctxt) [goal1, goal2, goal3]) end)
    1.73  end
    1.74  *}
    1.75  
    1.76  simproc_setup binary_int_div ("number_of m div number_of n :: int") =
    1.77 -  {* K (divmod_proc (@{thm divmod_int_rel_div_eq})) *}
    1.78 +  {* K (divmod_proc @{thm int_div_pos_eq} @{thm int_div_neg_eq}) *}
    1.79  
    1.80  simproc_setup binary_int_mod ("number_of m mod number_of n :: int") =
    1.81 -  {* K (divmod_proc (@{thm divmod_int_rel_mod_eq})) *}
    1.82 +  {* K (divmod_proc @{thm int_mod_pos_eq} @{thm int_mod_neg_eq}) *}
    1.83  
    1.84  lemmas posDivAlg_eqn_number_of [simp] =
    1.85      posDivAlg_eqn [of "number_of v" "number_of w", standard]