src/HOL/Divides.thy
changeset 45530 0c4853bb77bf
parent 45231 d85a2fdc586c
child 45607 16b4f5774621
equal deleted inserted replaced
45529:0e1037d4e049 45530:0c4853bb77bf
  1661      "[| a < 0;  b \<le> 0 |] ==> a mod b = snd (negateSnd (posDivAlg (-a) (-b)))"
  1661      "[| a < 0;  b \<le> 0 |] ==> a mod b = snd (negateSnd (posDivAlg (-a) (-b)))"
  1662 by (simp add: mod_int_def divmod_int_def)
  1662 by (simp add: mod_int_def divmod_int_def)
  1663 
  1663 
  1664 text {*Simplify expresions in which div and mod combine numerical constants*}
  1664 text {*Simplify expresions in which div and mod combine numerical constants*}
  1665 
  1665 
  1666 lemma divmod_int_relI:
  1666 lemma int_div_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a div b = q"
  1667   "\<lbrakk>a == b * q + r; if 0 < b then 0 \<le> r \<and> r < b else b < r \<and> r \<le> 0\<rbrakk>
  1667   by (rule divmod_int_rel_div [of a b q r],
  1668     \<Longrightarrow> divmod_int_rel a b (q, r)"
  1668     simp add: divmod_int_rel_def, simp)
  1669   unfolding divmod_int_rel_def by simp
  1669 
  1670 
  1670 lemma int_div_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a div b = q"
  1671 lemmas divmod_int_rel_div_eq = divmod_int_relI [THEN divmod_int_rel_div, THEN eq_reflection]
  1671   by (rule divmod_int_rel_div [of a b q r],
  1672 lemmas divmod_int_rel_mod_eq = divmod_int_relI [THEN divmod_int_rel_mod, THEN eq_reflection]
  1672     simp add: divmod_int_rel_def, simp)
       
  1673 
       
  1674 lemma int_mod_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a mod b = r"
       
  1675   by (rule divmod_int_rel_mod [of a b q r],
       
  1676     simp add: divmod_int_rel_def, simp)
       
  1677 
       
  1678 lemma int_mod_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a mod b = r"
       
  1679   by (rule divmod_int_rel_mod [of a b q r],
       
  1680     simp add: divmod_int_rel_def, simp)
       
  1681 
  1673 lemmas arithmetic_simps =
  1682 lemmas arithmetic_simps =
  1674   arith_simps
  1683   arith_simps
  1675   add_special
  1684   add_special
  1676   add_0_left
  1685   add_0_left
  1677   add_0_right
  1686   add_0_right
  1681   mult_1_right
  1690   mult_1_right
  1682 
  1691 
  1683 (* simprocs adapted from HOL/ex/Binary.thy *)
  1692 (* simprocs adapted from HOL/ex/Binary.thy *)
  1684 ML {*
  1693 ML {*
  1685 local
  1694 local
  1686   val mk_number = HOLogic.mk_number HOLogic.intT;
  1695   val mk_number = HOLogic.mk_number HOLogic.intT
  1687   fun mk_cert u k l = @{term "plus :: int \<Rightarrow> int \<Rightarrow> int"} $
  1696   val plus = @{term "plus :: int \<Rightarrow> int \<Rightarrow> int"}
  1688     (@{term "times :: int \<Rightarrow> int \<Rightarrow> int"} $ u $ mk_number k) $
  1697   val times = @{term "times :: int \<Rightarrow> int \<Rightarrow> int"}
  1689       mk_number l;
  1698   val zero = @{term "0 :: int"}
  1690   fun prove ctxt prop = Goal.prove ctxt [] [] prop
  1699   val less = @{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"}
  1691     (K (ALLGOALS (full_simp_tac (HOL_basic_ss addsimps @{thms arithmetic_simps}))));
  1700   val le = @{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"}
       
  1701   val simps = @{thms arith_simps} @ @{thms rel_simps} @
       
  1702     map (fn th => th RS sym) [@{thm numeral_0_eq_0}, @{thm numeral_1_eq_1}]
       
  1703   fun prove ctxt goal = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop goal)
       
  1704     (K (ALLGOALS (full_simp_tac (HOL_basic_ss addsimps simps))));
  1692   fun binary_proc proc ss ct =
  1705   fun binary_proc proc ss ct =
  1693     (case Thm.term_of ct of
  1706     (case Thm.term_of ct of
  1694       _ $ t $ u =>
  1707       _ $ t $ u =>
  1695       (case try (pairself (`(snd o HOLogic.dest_number))) (t, u) of
  1708       (case try (pairself (`(snd o HOLogic.dest_number))) (t, u) of
  1696         SOME args => proc (Simplifier.the_context ss) args
  1709         SOME args => proc (Simplifier.the_context ss) args
  1697       | NONE => NONE)
  1710       | NONE => NONE)
  1698     | _ => NONE);
  1711     | _ => NONE);
  1699 in
  1712 in
  1700   fun divmod_proc rule = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
  1713   fun divmod_proc posrule negrule =
  1701     if n = 0 then NONE
  1714     binary_proc (fn ctxt => fn ((a, t), (b, u)) =>
  1702     else let val (k, l) = Integer.div_mod m n;
  1715       if b = 0 then NONE else let
  1703     in SOME (rule OF [prove ctxt (Logic.mk_equals (t, mk_cert u k l))]) end);
  1716         val (q, r) = pairself mk_number (Integer.div_mod a b)
       
  1717         val goal1 = HOLogic.mk_eq (t, plus $ (times $ u $ q) $ r)
       
  1718         val (goal2, goal3, rule) = if b > 0
       
  1719           then (le $ zero $ r, less $ r $ u, posrule RS eq_reflection)
       
  1720           else (le $ r $ zero, less $ u $ r, negrule RS eq_reflection)
       
  1721       in SOME (rule OF map (prove ctxt) [goal1, goal2, goal3]) end)
  1704 end
  1722 end
  1705 *}
  1723 *}
  1706 
  1724 
  1707 simproc_setup binary_int_div ("number_of m div number_of n :: int") =
  1725 simproc_setup binary_int_div ("number_of m div number_of n :: int") =
  1708   {* K (divmod_proc (@{thm divmod_int_rel_div_eq})) *}
  1726   {* K (divmod_proc @{thm int_div_pos_eq} @{thm int_div_neg_eq}) *}
  1709 
  1727 
  1710 simproc_setup binary_int_mod ("number_of m mod number_of n :: int") =
  1728 simproc_setup binary_int_mod ("number_of m mod number_of n :: int") =
  1711   {* K (divmod_proc (@{thm divmod_int_rel_mod_eq})) *}
  1729   {* K (divmod_proc @{thm int_mod_pos_eq} @{thm int_mod_neg_eq}) *}
  1712 
  1730 
  1713 lemmas posDivAlg_eqn_number_of [simp] =
  1731 lemmas posDivAlg_eqn_number_of [simp] =
  1714     posDivAlg_eqn [of "number_of v" "number_of w", standard]
  1732     posDivAlg_eqn [of "number_of v" "number_of w", standard]
  1715 
  1733 
  1716 lemmas negDivAlg_eqn_number_of [simp] =
  1734 lemmas negDivAlg_eqn_number_of [simp] =