# HG changeset patch # User huffman # Date 1321453227 -3600 # Node ID 0c4853bb77bf5b1dcf1b56cbf118631836433663 # Parent 0e1037d4e049e9f20ddf90e349f8bb7950195ffe rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests diff -r 0e1037d4e049 -r 0c4853bb77bf src/HOL/Divides.thy --- a/src/HOL/Divides.thy Wed Nov 16 13:58:31 2011 +0100 +++ b/src/HOL/Divides.thy Wed Nov 16 15:20:27 2011 +0100 @@ -1663,13 +1663,22 @@ text {*Simplify expresions in which div and mod combine numerical constants*} -lemma divmod_int_relI: - "\a == b * q + r; if 0 < b then 0 \ r \ r < b else b < r \ r \ 0\ - \ divmod_int_rel a b (q, r)" - unfolding divmod_int_rel_def by simp - -lemmas divmod_int_rel_div_eq = divmod_int_relI [THEN divmod_int_rel_div, THEN eq_reflection] -lemmas divmod_int_rel_mod_eq = divmod_int_relI [THEN divmod_int_rel_mod, THEN eq_reflection] +lemma int_div_pos_eq: "\(a::int) = b * q + r; 0 \ r; r < b\ \ a div b = q" + by (rule divmod_int_rel_div [of a b q r], + simp add: divmod_int_rel_def, simp) + +lemma int_div_neg_eq: "\(a::int) = b * q + r; r \ 0; b < r\ \ a div b = q" + by (rule divmod_int_rel_div [of a b q r], + simp add: divmod_int_rel_def, simp) + +lemma int_mod_pos_eq: "\(a::int) = b * q + r; 0 \ r; r < b\ \ a mod b = r" + by (rule divmod_int_rel_mod [of a b q r], + simp add: divmod_int_rel_def, simp) + +lemma int_mod_neg_eq: "\(a::int) = b * q + r; r \ 0; b < r\ \ a mod b = r" + by (rule divmod_int_rel_mod [of a b q r], + simp add: divmod_int_rel_def, simp) + lemmas arithmetic_simps = arith_simps add_special @@ -1683,12 +1692,16 @@ (* simprocs adapted from HOL/ex/Binary.thy *) ML {* local - val mk_number = HOLogic.mk_number HOLogic.intT; - fun mk_cert u k l = @{term "plus :: int \ int \ int"} $ - (@{term "times :: int \ int \ int"} $ u $ mk_number k) $ - mk_number l; - fun prove ctxt prop = Goal.prove ctxt [] [] prop - (K (ALLGOALS (full_simp_tac (HOL_basic_ss addsimps @{thms arithmetic_simps})))); + val mk_number = HOLogic.mk_number HOLogic.intT + val plus = @{term "plus :: int \ int \ int"} + val times = @{term "times :: int \ int \ int"} + val zero = @{term "0 :: int"} + val less = @{term "op < :: int \ int \ bool"} + val le = @{term "op \ :: int \ int \ bool"} + val simps = @{thms arith_simps} @ @{thms rel_simps} @ + map (fn th => th RS sym) [@{thm numeral_0_eq_0}, @{thm numeral_1_eq_1}] + fun prove ctxt goal = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop goal) + (K (ALLGOALS (full_simp_tac (HOL_basic_ss addsimps simps)))); fun binary_proc proc ss ct = (case Thm.term_of ct of _ $ t $ u => @@ -1697,18 +1710,23 @@ | NONE => NONE) | _ => NONE); in - fun divmod_proc rule = binary_proc (fn ctxt => fn ((m, t), (n, u)) => - if n = 0 then NONE - else let val (k, l) = Integer.div_mod m n; - in SOME (rule OF [prove ctxt (Logic.mk_equals (t, mk_cert u k l))]) end); + fun divmod_proc posrule negrule = + binary_proc (fn ctxt => fn ((a, t), (b, u)) => + if b = 0 then NONE else let + val (q, r) = pairself mk_number (Integer.div_mod a b) + val goal1 = HOLogic.mk_eq (t, plus $ (times $ u $ q) $ r) + val (goal2, goal3, rule) = if b > 0 + then (le $ zero $ r, less $ r $ u, posrule RS eq_reflection) + else (le $ r $ zero, less $ u $ r, negrule RS eq_reflection) + in SOME (rule OF map (prove ctxt) [goal1, goal2, goal3]) end) end *} simproc_setup binary_int_div ("number_of m div number_of n :: int") = - {* K (divmod_proc (@{thm divmod_int_rel_div_eq})) *} + {* K (divmod_proc @{thm int_div_pos_eq} @{thm int_div_neg_eq}) *} simproc_setup binary_int_mod ("number_of m mod number_of n :: int") = - {* K (divmod_proc (@{thm divmod_int_rel_mod_eq})) *} + {* K (divmod_proc @{thm int_mod_pos_eq} @{thm int_mod_neg_eq}) *} lemmas posDivAlg_eqn_number_of [simp] = posDivAlg_eqn [of "number_of v" "number_of w", standard] diff -r 0e1037d4e049 -r 0c4853bb77bf src/HOL/ex/Simproc_Tests.thy --- a/src/HOL/ex/Simproc_Tests.thy Wed Nov 16 13:58:31 2011 +0100 +++ b/src/HOL/ex/Simproc_Tests.thy Wed Nov 16 15:20:27 2011 +0100 @@ -420,9 +420,11 @@ assume "4*k = u" have "k + 3*k = u" by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact next + (* FIXME "Suc (i + 3) \ i + 4" *) assume "4 * Suc 0 + i = u" have "Suc (i + 3) = u" by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact next + (* FIXME "Suc (i + j + 3 + k) \ i + j + 4 + k" *) assume "4 * Suc 0 + (i + (j + k)) = u" have "Suc (i + j + 3 + k) = u" by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact next @@ -712,4 +714,43 @@ } end +subsection {* Integer numeral div/mod simprocs *} + +notepad begin + have "(10::int) div 3 = 3" + by (tactic {* test [@{simproc binary_int_div}] *}) + have "(10::int) mod 3 = 1" + by (tactic {* test [@{simproc binary_int_mod}] *}) + have "(10::int) div -3 = -4" + by (tactic {* test [@{simproc binary_int_div}] *}) + have "(10::int) mod -3 = -2" + by (tactic {* test [@{simproc binary_int_mod}] *}) + have "(-10::int) div 3 = -4" + by (tactic {* test [@{simproc binary_int_div}] *}) + have "(-10::int) mod 3 = 2" + by (tactic {* test [@{simproc binary_int_mod}] *}) + have "(-10::int) div -3 = 3" + by (tactic {* test [@{simproc binary_int_div}] *}) + have "(-10::int) mod -3 = -1" + by (tactic {* test [@{simproc binary_int_mod}] *}) + have "(8452::int) mod 3 = 1" + by (tactic {* test [@{simproc binary_int_mod}] *}) + have "(59485::int) div 434 = 137" + by (tactic {* test [@{simproc binary_int_div}] *}) + have "(1000006::int) mod 10 = 6" + by (tactic {* test [@{simproc binary_int_mod}] *}) + have "10000000 div 2 = (5000000::int)" + by (tactic {* test [@{simproc binary_int_div}] *}) + have "10000001 mod 2 = (1::int)" + by (tactic {* test [@{simproc binary_int_mod}] *}) + have "10000055 div 32 = (312501::int)" + by (tactic {* test [@{simproc binary_int_div}] *}) + have "10000055 mod 32 = (23::int)" + by (tactic {* test [@{simproc binary_int_mod}] *}) + have "100094 div 144 = (695::int)" + by (tactic {* test [@{simproc binary_int_div}] *}) + have "100094 mod 144 = (14::int)" + by (tactic {* test [@{simproc binary_int_mod}] *}) end + +end