rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
authorhuffman
Wed Nov 16 15:20:27 2011 +0100 (2011-11-16)
changeset 455300c4853bb77bf
parent 45529 0e1037d4e049
child 45531 528bad46f29e
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
src/HOL/Divides.thy
src/HOL/ex/Simproc_Tests.thy
     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]
     2.1 --- a/src/HOL/ex/Simproc_Tests.thy	Wed Nov 16 13:58:31 2011 +0100
     2.2 +++ b/src/HOL/ex/Simproc_Tests.thy	Wed Nov 16 15:20:27 2011 +0100
     2.3 @@ -420,9 +420,11 @@
     2.4      assume "4*k = u" have "k + 3*k = u"
     2.5        by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
     2.6    next
     2.7 +    (* FIXME "Suc (i + 3) \<equiv> i + 4" *)
     2.8      assume "4 * Suc 0 + i = u" have "Suc (i + 3) = u"
     2.9        by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
    2.10    next
    2.11 +    (* FIXME "Suc (i + j + 3 + k) \<equiv> i + j + 4 + k" *)
    2.12      assume "4 * Suc 0 + (i + (j + k)) = u" have "Suc (i + j + 3 + k) = u"
    2.13        by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
    2.14    next
    2.15 @@ -712,4 +714,43 @@
    2.16    }
    2.17  end
    2.18  
    2.19 +subsection {* Integer numeral div/mod simprocs *}
    2.20 +
    2.21 +notepad begin
    2.22 +  have "(10::int) div 3 = 3"
    2.23 +    by (tactic {* test [@{simproc binary_int_div}] *})
    2.24 +  have "(10::int) mod 3 = 1"
    2.25 +    by (tactic {* test [@{simproc binary_int_mod}] *})
    2.26 +  have "(10::int) div -3 = -4"
    2.27 +    by (tactic {* test [@{simproc binary_int_div}] *})
    2.28 +  have "(10::int) mod -3 = -2"
    2.29 +    by (tactic {* test [@{simproc binary_int_mod}] *})
    2.30 +  have "(-10::int) div 3 = -4"
    2.31 +    by (tactic {* test [@{simproc binary_int_div}] *})
    2.32 +  have "(-10::int) mod 3 = 2"
    2.33 +    by (tactic {* test [@{simproc binary_int_mod}] *})
    2.34 +  have "(-10::int) div -3 = 3"
    2.35 +    by (tactic {* test [@{simproc binary_int_div}] *})
    2.36 +  have "(-10::int) mod -3 = -1"
    2.37 +    by (tactic {* test [@{simproc binary_int_mod}] *})
    2.38 +  have "(8452::int) mod 3 = 1"
    2.39 +    by (tactic {* test [@{simproc binary_int_mod}] *})
    2.40 +  have "(59485::int) div 434 = 137"
    2.41 +    by (tactic {* test [@{simproc binary_int_div}] *})
    2.42 +  have "(1000006::int) mod 10 = 6"
    2.43 +    by (tactic {* test [@{simproc binary_int_mod}] *})
    2.44 +  have "10000000 div 2 = (5000000::int)"
    2.45 +    by (tactic {* test [@{simproc binary_int_div}] *})
    2.46 +  have "10000001 mod 2 = (1::int)"
    2.47 +    by (tactic {* test [@{simproc binary_int_mod}] *})
    2.48 +  have "10000055 div 32 = (312501::int)"
    2.49 +    by (tactic {* test [@{simproc binary_int_div}] *})
    2.50 +  have "10000055 mod 32 = (23::int)"
    2.51 +    by (tactic {* test [@{simproc binary_int_mod}] *})
    2.52 +  have "100094 div 144 = (695::int)"
    2.53 +    by (tactic {* test [@{simproc binary_int_div}] *})
    2.54 +  have "100094 mod 144 = (14::int)"
    2.55 +    by (tactic {* test [@{simproc binary_int_mod}] *})
    2.56  end
    2.57 +
    2.58 +end